coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-12-03	Removing useless meta-related functions.	Pierre-Marie Pédrot
2013-11-02	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-18	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-05-14	Mini documentation (evar_absorb_arguments).	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-02-10	Splitted Evarutil in two files	ppedrot
2013-02-10	Moved code from Pretype_error to Evarutil	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-08-08	Updating headers.	herbelin
2012-07-10	Another correction to the dependent existential variable printing	aspiwack
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-03-20	Generalized the use of evar candidates in type inference unification:	herbelin
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-03-02	Noise for nothing	pboutill
2011-12-16	Introducing a notion of evar candidates to be used when an evar is	herbelin
2011-12-04	Discarding let-ins from the instances of the evars in the	herbelin
2011-11-23	Adds a pair of function in Evar_util to gather dependent evars in an	aspiwack
2011-11-06	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin
2011-10-25	Continuing r1492 (useless changes were inadvertantly committed)	herbelin
2011-10-25	New strategy to infer return predicate of match construct when	herbelin
2011-10-10	More robust and uniform treatment of aliases in evarutil.ml	herbelin
2011-10-10	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin
2011-10-10	Passed conv_algo to evar_define and move call to solve_refl to	herbelin
2011-06-07	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-11	- Better error messages taking unif. constraints into account.	msozeau
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-03-05	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin
2011-02-03	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey
2011-01-07	mli comments for doc	pboutill
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-15	Misc improvements about evar_map	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin