Karl Palmskog (Feb 15 2022 at 11:31): Karl Palmskog (Feb 15 2022 at 11:31):@Hugo Herbelin I was hoping to start work today on a PR for adding Body as a synonym for Proof. How would you advise to begin that work? In ppvernac.ml or somewhere else?
Hugo Herbelin (Feb 15 2022 at 11:32):Already in g_vernac.mlg for the parsing.
Hugo Herbelin (Feb 15 2022 at 11:36):Sorry, in plugins/ltac/g_ltac.mlg.
Hugo Herbelin (Feb 15 2022 at 11:36):Where you have the syntax for Proof.
Hugo Herbelin (Feb 15 2022 at 11:48):Then, if you want it to be printed Body, you need to extend VernacProof in vernacexpr.ml with an information telling if it is Body or Proof (a Boolean, or even an enumerated type type start_proof_style = Proof | Body), and use this information in ppvernac.ml indeed.
Karl Palmskog (Feb 15 2022 at 11:49):hmm, then maybe I'll try just allowing Body as input as a first step
Hugo Herbelin (Feb 15 2022 at 11:50):Yes, sure.
Théo Zimmermann (Feb 15 2022 at 13:06):You might also need to tweak coqdoc so that it knows about this new command...
Théo Zimmermann (Feb 15 2022 at 13:07):Especially given that this is done with documentation purpose in mind.
Last updated: Jun 11 2023 at 00:30 UTC