coq - The formal proof system

Age	Commit message (Expand)	Author
2011-11-17	Fixing new bug introduced in r14665 when fixing bug #1834.	herbelin
2011-11-16	Adding postprocessing to remove "commutative cuts" expansions in	herbelin
2011-11-16	Changed the way find_dependencies_signature is working so that it	herbelin
2011-11-16	De Bruijn indices bug in pattern matching compilation in the presence	herbelin
2011-11-16	Old generalization bug in pattern-matching: names were considered the	herbelin
2011-11-16	Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).	herbelin
2011-11-16	Old typing bug in pattern-matching compilation (apparently w/o	herbelin
2011-11-16	Specialization of tomatch in pattern-matching compilation was done too	herbelin
2011-11-16	A bit of documentation around cases.ml + ML modules uselessly open	herbelin
2011-11-16	Fixing dependencies lifting bug in pattern-matching compilation	herbelin
2011-10-25	Fixing use of type constraint for refining the "return" clause of "match".	herbelin
2011-10-25	New strategy to infer return predicate of match construct when	herbelin
2011-10-05	It happens that the type inference algorithm (pretyping) did not check	herbelin
2011-08-08	Two bugs in pattern-matching compilation:	herbelin
2011-07-29	Cases: generic equality on constr replaced by destructors	puech
2011-03-13	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-19	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin
2010-10-06	Fixing the Not_found error in bug #2404 + dead code removal in cases.ml	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-12	Improved the inference of the return predicate in dependent pattern-matching.	herbelin
2010-06-11	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin
2010-06-10	Fixed two bugs in pattern-matching compilation	herbelin
2010-05-20	Fix bug 2307	pboutill
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-12-30	Fixing bug #2193: computation of dependencies in the "match" return	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-28	Improve return predicate inference by making the return type dependent	msozeau
2009-06-06	Fixing bug #2106 ("match" compilation with multi-dependent constructor).	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-11-27	Fix (?) a pattern matching compilation problem:	msozeau
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-10	- Correction bug 1841 (identificateurs incorrects avec Subclass)	herbelin