coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
*	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
*	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed	2017-02-16
*	Making the grammar/ folder independent from the other ones.	Pierre-Marie Pédrot	2016-05-31
*	Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.	Pierre-Marie Pédrot	2016-05-14
*	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
*	Fixing compilation with old versions of CAMLP5.	Pierre-Marie Pédrot	2016-03-19
*	EXTEND macros use their own internal representations.	Pierre-Marie Pédrot	2016-03-19
*	Do not keep the argument type in ExtNonTerminal.	Pierre-Marie Pédrot	2016-03-19
*	Making the EXTEND macros almost self-contained.	Pierre-Marie Pédrot	2016-03-18
*	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Removing dead code in Q_util.	Pierre-Marie Pédrot	2016-03-17
*	Reducing the number of modules linked in grammar.cma.	Pierre-Marie Pédrot	2016-03-17
*	Removing the Q_coqast module.	Pierre-Marie Pédrot	2016-02-24
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	ML extensions use untyped representation of user entries.	Pierre-Marie Pédrot	2016-01-17
* \|	Proper datatype for EXTEND syntax tokens.	Pierre-Marie Pédrot	2016-01-02
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Updating headers.	herbelin	2012-08-08
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29