coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-13	Fixing #4467 (continued).	Hugo Herbelin
2016-01-12	Fixing #4467 (missing shadowing of variables in cases pattern).	Hugo Herbelin
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-06-17	Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).	Hugo Herbelin
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
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-14	Modulification of identifier	ppedrot
2012-11-25	Monomorphization (interp)	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	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-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-06-04	Replacing some str with strbrk	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	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-15	Notations are back in the "in" clause of pattern matching.	pboutill
2012-04-12	"A -> B" is a notation for "forall _ : A, B".	pboutill
2012-04-06	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin
2012-03-20	Fixing bug #2724 (using notations with binders in cases patterns	herbelin
2012-03-02	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill
2012-03-02	Noise for nothing	pboutill
2012-02-29	In the syntax of pattern matching, "in" clauses are patterns.	pboutill
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-19	Boolean Option Patterns Compatibility	pboutill
2012-01-16	Parameters in pattern first step.	pboutill
2011-12-16	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2011-08-30	Quick improvement of some error messages related to module application	herbelin
2011-07-22	Add a syntax entry for fully applied constructor pattern	pboutill
2011-06-12	Rather quick hack to avoid using notations involving "Type" when	herbelin
2011-06-08	Make Notation works with anonymous-level "Type".	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-02-11	Annotations at functor applications:	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu