coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-11-06	Removing dead code in Plexing.	Pierre-Marie Pédrot
	It was full with utility functions and wrappers that are unused in the Coq codebase.
2018-11-06	Remove the non-functorial interface of camlp5 grammars.	Pierre-Marie Pédrot

2018-11-05	Remove patches of dead code in 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-11-04	Remove the deprecated Token module and port the corresponding code.	Pierre-Marie Pédrot

2018-10-29	[gramlib] Wrap `Gramlib`.	Emilio Jesus Gallego Arias
	This introduces a bit of noise in the Dune files but for now I think it is the best way to do it.
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