coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
* \|	[location] Remove `Loc.internal_ghost`	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
* \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \|	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
* \|	Getting rid of most uses of unsafe_grammar_extend.	Pierre-Marie Pédrot	2015-10-27
* \|	Type-safe Egramml.make_rule.	Pierre-Marie Pédrot	2015-10-27
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	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
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	Moving the ML tactic extension mechanism to a Libobject-based one.	Pierre-Marie Pédrot	2014-05-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
*	Modulification of identifier	ppedrot	2012-12-14
*	Egramml: minor simplification	letouzey	2012-10-15
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Split Egrammar into Egramml and Egramcoq	letouzey	2012-05-29