Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Body as synonym for Proof


view this post on Zulip 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?

view this post on Zulip Hugo Herbelin (Feb 15 2022 at 11:32):

Already in g_vernac.mlg for the parsing.

view this post on Zulip Hugo Herbelin (Feb 15 2022 at 11:36):

Sorry, in plugins/ltac/g_ltac.mlg.

view this post on Zulip Hugo Herbelin (Feb 15 2022 at 11:36):

Where you have the syntax for Proof.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 15 2022 at 11:49):

hmm, then maybe I'll try just allowing Body as input as a first step

view this post on Zulip Hugo Herbelin (Feb 15 2022 at 11:50):

Yes, sure.

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 13:06):

You might also need to tweak coqdoc so that it knows about this new command...

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 13:07):

Especially given that this is done with documentation purpose in mind.


Last updated: Jan 29 2023 at 15:02 UTC