coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|/
*	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
* \|	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
* \|	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
*	More comments in Genarg.	ppedrot	2013-06-06
*	Modulification of identifier	ppedrot	2012-12-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