coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-18	COMMENTS: added to some variants of "Glob_term.glob_constr" type.	Matej Kosik
2015-01-12	Update headers.	Maxime Dénès
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-12	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-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-09-05	Ltac's [uconstr] values now use the identifier context to give names to binders.	Arnaud Spiwack
2014-08-06	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-02	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey
2012-08-24	Correcting a comment in pattern-matching compilation.	aspiwack
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	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