coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík	2017-05-24
*	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
*	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
*	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
*	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
*	Using the same type of binders for interning and externing.	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
*	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
*	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	COMMENTS: added to some variants of "Glob_term.glob_constr" type.	Matej Kosik	2015-12-18
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Ltac's [uconstr] values now use the identifier context to give names to binders.	Arnaud Spiwack	2014-09-05
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey	2012-10-02
*	Correcting a comment in pattern-matching compilation.	aspiwack	2012-08-24
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Glob_term: minor formatting	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29