coq - The formal proof system

Age	Commit message (Expand)	Author
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-05-31	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin
2017-05-24	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík
2017-04-25	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
2017-04-24	[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-03-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
2016-09-22	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès
2016-09-20	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès
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