coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|/ \| \| \| \|	`internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
*	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
\| \| \| \| \| \| \| \|	Actually the identifier was never used and just carried along.
* \|	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
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
\| \| \| \| \| \| \| \| \| \|	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Split Egrammar into Egramml and Egramcoq	letouzey	2012-05-29
	Two gains: - no Summary in Grammar.cma - get rid of the hack concerning error_invalid_pattern_notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7