coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Notations with binders: Accepting using notations for functional terms	herbelin	2012-01-20
*	Boolean Option Patterns Compatibility	pboutill	2012-01-19
*	Parameters in pattern first step.	pboutill	2012-01-16
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Rather quick hack to avoid using notations involving "Type" when	herbelin	2011-06-12
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	Annotations at functor applications:	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin	2010-12-04
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22