coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Allowing to pass arbitrary data in internalization environments.	Pierre-Marie Pédrot	2017-05-03
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
\| *	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
\| *	Merging glob_binder and glob_decl.	Hugo Herbelin	2017-03-24
\| *	Cleaning phase around local binder at glob level:	Hugo Herbelin	2017-03-24
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
*	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Documenting a bit more interpretation functions in passing.	Hugo Herbelin	2015-10-26
*	Fixing computation of implicit arguments by position in fixpoints (#4217).	Hugo Herbelin	2015-05-01
*	Function now supports puniveres	jforest	2015-04-14
*	Update headers.	Maxime Dénès	2015-01-12
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Revert the change in Constrintern introduced by "Add a type of untyped term t...	Arnaud Spiwack	2014-08-06
*	Better struture for Ltac internalization environments in Constrintern.	Pierre-Marie Pédrot	2014-08-02
*	Faster uconstr.	Arnaud Spiwack	2014-08-01
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Useless use of maps in constr internalizing.	ppedrot	2013-06-25
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	More equality functions	ppedrot	2012-11-25
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	local variables can have implicits locally	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	More comments and less doublons in some mli	pboutill	2011-02-10