coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-12-22	Ensure that a custom entry cannot be defined twice.	Pierre-Marie Pédrot
	This highlights the fact that diamond inheritance of a custom entry is a tricky problem, as well as merely importing two custom entries with the same name from two different modules. The only sane way to give a semantics to that is to stick to module-scoped objects, i.e. give those entries a kernel name. In the meantime, I went for a warning when overriding entries.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-07-29	Store marshallable data in the custom entry summary.	Pierre-Marie Pédrot

2018-05-31	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias
	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
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.