coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-22
\|\
\| *	Turning an anomaly on 'pat into a proper "unsupported" error message.	Hugo Herbelin	2017-02-09
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\|\\|
\| *	Fixing #5326 (anomaly on some unsupported case of 'pat).	Hugo Herbelin	2017-01-26
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\|
\| *	Shorter message for "Test Asymmetric Patterns".	Hugo Herbelin	2016-10-12
* \|	Fix an error-prone error API.	Pierre-Marie Pédrot	2016-09-21
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Reformatting + removal of some useless data + some cut-elimination	Hugo Herbelin	2016-04-27
*	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
*	A more explicit name to the asymmetric boolean flag.	Hugo Herbelin	2016-03-12
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
\| *	Fixing #4467 (missing shadowing of variables in cases pattern).	Hugo Herbelin	2016-01-12
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	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
*	Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).	Hugo Herbelin	2014-06-17
*	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
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (interp)	ppedrot	2012-11-25
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	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
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Notations are back in the "in" clause of pattern matching.	pboutill	2012-05-15
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12