coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-11	Move most of Gramext into Grammar.	Pierre-Marie Pédrot
	This module was defining unsafe functions and datatypes only relevant to the grammar engine. We hide them under the API so as to be able to later clean it up.
2018-12-05	Remove the Like level modifier from gramlib.	Pierre-Marie Pédrot
	Apart from the fact we did not use it, its semantics was somewhat flaky as it was looking for any rule containing some token.
2018-12-05	Remove the grammar-entry correspondence dynamic check in camlp5.	Pierre-Marie Pédrot
	Due to the fact we only export the functorial API, this property is ensured statically. There is thus no point in checking it.
2018-12-05	Make some camlp5 fields immutable.	Pierre-Marie Pédrot

2018-11-27	[gramlib] Remove unused function `gram_reinit`.	Emilio Jesus Gallego Arias

2018-11-27	[gramlib] Minor cleanups:	Emilio Jesus Gallego Arias
	- remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter.
2018-11-23	Remove the unsafe API from gramlib.	Pierre-Marie Pédrot

2018-11-05	Remove the Scut constructor from Gramlib.	Pierre-Marie Pédrot
	This constructor only makes sense in the backtracking mode, that has been removed from our vendored version of camlp5.
2018-11-05	Remove the Sflag constructor from Gramlib.	Pierre-Marie Pédrot
	It is just a wrapper around Sopt. I do not really understand why it is hardwired in the entry AST.
2018-11-05	Remove the Sfacto constructor from Gramlib.	Pierre-Marie Pédrot
	Used by rule factorisation in theory, but appears to be unused in Coq.
2018-11-05	Remove the Svala constructor from Gramlib.	Pierre-Marie Pédrot
	It is only used in strict mode, which makes no sense for Coq grammar.
2018-11-05	Remove Smeta constructor in Gramlib.	Pierre-Marie Pédrot
	This constructor was only used by meta-level macros that are not used and serve no purpose in the grammar engine.
2018-10-29	[gramlib] Cleanup, remove unused parsing infrastructure.	Emilio Jesus Gallego Arias
	We remove the functional and backtracking parsers as they are not used in Coq.
2018-10-29	[camlp5] Fix warnings, switch Coq to vendored library.	Emilio Jesus Gallego Arias

2018-10-29	[camlp5] Automatic conversion from revised syntax + parsers	Emilio Jesus Gallego Arias
	`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
2018-10-29	[gramlib] Original Import from Camlp5 repos.	Emilio Jesus Gallego Arias