Stream: Coq users

Topic: Braces outside proofs

view this post on Zulip Clément Pit-Claudel (Aug 08 2020 at 04:10):

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?

view this post on Zulip Paolo Giarrusso (Aug 08 2020 at 08:15):

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

view this post on Zulip Théo Zimmermann (Aug 08 2020 at 09:38):

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

Last updated: Sep 23 2023 at 14:01 UTC