coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-02	Reverted an incorrect code simplification in function status_changed	herbelin
2009-10-30	Attempt to capture on time unification errors for "with" bindings.	herbelin
2009-10-30	Take constraints into account in the "instantiate" tactic	herbelin
2009-10-29	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-10-28	Make usage of Dyn explicit	glondu
2009-10-27	Fixes around typeclasses:	msozeau
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-23	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	herbelin
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-08-23	A new kind of automatically generated scheme "congr" for equality types	herbelin
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-13	Made unification patch 12268 even more ad hoc (if evars remain in a	herbelin
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau
2009-07-08	Fixed bug #2116 ("simpl" created ill-typed term while accepting	herbelin
2009-07-08	Don't use recent ocaml tolerance for pattern "ProjectVar _" when	herbelin
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-08	Add heuristic based on non-linearity of evars to determine whether an	herbelin
2009-07-08	Fixing bug 2129 (evar introduced to remember an ambiguous projection	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-07-06	change in the order of unification constraints solving (for canonical structu...	amahboub
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-06-28	Improve return predicate inference by making the return type dependent	msozeau
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-22	documented a bug of pattern unification with metas	barras
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-18	Try typeclass resolution in coercion if no solution can be found to a	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-11	When typing a non-dependent arrow, do not put the (anonymous) variable	msozeau
2009-06-06	Fixing bug #2106 ("match" compilation with multi-dependent constructor).	herbelin
2009-06-02	Adding a regression test about Bauer's example on coq-club of	herbelin
2009-06-02	Backtrack on experimental unification with sort variables: it requires	msozeau
2009-06-01	Change unification with sort constraints to not use the kernel	msozeau
2009-05-28	Properly catch sort constraint inconsistency exception in	msozeau
2009-05-27	Populate the sort constraints set correctly during unification. Add a	msozeau
2009-05-24	Temporary fixes in unification:	msozeau