I just noticed that Coq accepts braces (edit: and bullets) outside proofs, and they don't need to be matched, either: `} --- Proof. { + + - { ** Definition a := 1. }}}}} Proof. Proof. { + -`

is a valid script that means the same as `Definition a := 1.`

. Do they mean anything or are they no-ops just like `Proof`

?

- IMHO that's a bug, I've seen it before l
- Proof. is not a noop; it affects async proofs, especially in sections and when using Set Default Proof Using..., which only affects Proof.

Yes, it's a known issue. Cf. coq/coq#12004.

Last updated: Sep 23 2023 at 14:01 UTC