coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-23	Relying on the abstract notion of streams with location for parsing.	Hugo Herbelin
	We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml).
2021-04-23	Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.	Hugo Herbelin

2020-07-16	[gramlib] Remove legacy located exception wrapper in favor of standard ↵	Emilio Jesus Gallego Arias
	infrastructure. The old wrapper was basically unused, this PR also fixes backtraces in some class of bugs such as https://github.com/coq/coq/issues/12695
2019-02-05	Remove the comment fields of locations.	Pierre-Marie Pédrot
	They didn't seem to be used at all.
2018-11-30	[gramlib] Remove `Ploc.t` in favor of `Loc.t`	Emilio Jesus Gallego Arias
	The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option`
2018-11-05	Remove patches of dead code in Gramlib.	Pierre-Marie Pédrot

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-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] 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