coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-07	[abbreviation] allow the user to set arguments scope	Enrico Tassi

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-23	[vernacexpr] Refactor fixpoint AST.	Emilio Jesus Gallego Arias
	We turn the tuples used for (co)-fixpoints into records, cleaning up their users. More cleanup is be possible, in particular a few functions can now shared among co and fixpoints, also `structured_fixpoint_expr` could like be folded into the new record. Feedback on the naming of the records fields is welcome. This is a step towards cleaning up code in `funind`, as it is the main consumer of this data structure, as it does quite a bit of fixpoint manipulation. cc: #6019
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-05-27	[api] [parsing] Move Egram* to `vernac/`	Emilio Jesus Gallego Arias
	The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin.