coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-04-12	Unify Set and Unset handling for options	Gaëtan Gilbert
	Not sure if the idetop.set_options was correctly changed, ocaml types pass at least.
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert

2018-07-13	Remove useless libobject in proof_using	Maxime Dénès

2018-07-07	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot
	We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
2017-10-10	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert

2017-10-10	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert

2017-10-10	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias
	We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.