coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #7898: Remove camlp4 remains	Emilio Jesus Gallego Arias	2018-07-11
\|\
\| *	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.
* \|	fix syntax of .mlg	Vincent Laporte	2018-07-03
\| \|
* \|	[vernac] use plain strings as attribute names	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|	The concrete syntax is still restricted to identifiers.
* \|	[vernac] indentation	Vincent Laporte	2018-07-03
\| \|
* \|	[vernac] Generic syntax for flags/attributes	Vincent Laporte	2018-07-03
\| \|
* \|	[vernac] Generic parsing rules for attributes	Vincent Laporte	2018-07-03
\| \|
* \|	[vernac] Concrete syntax for attributes	Vincent Laporte	2018-07-03
\|/
*	Port g_vernac to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29