coq - The formal proof system

Age	Commit message (Expand)	Author
2016-06-27	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre
2016-03-13	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin
2016-03-13	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin
2016-01-29	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-23	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	COMMENTS: added to the "Constrexpr.CCases" variant.	Matej Kosik
2016-01-11	CLEANUP: removing unused field	Matej Kosik
2015-12-18	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik
2015-12-18	COMMENTS: added to some variants of the "Constrexpr.prim_token" 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-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-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-12-14	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot
2012-10-02	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-14	Internalization of pattern is done in two phases.	pboutill
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey