coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove useless libobject in proof_using	Maxime Dénès	2018-07-13
\|
*	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot	2018-07-07
\| \| \| \| \| \| \| \| \| \|	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.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	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.
*	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	2017-10-10
	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.