coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-20	Many fixes in unification:	msozeau
2009-05-19	Fix in canonical structure resolution: [check_conv_record] may return	msozeau
2009-05-19	Remove camlp4-specific exception handling	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-05-16	(Tentative to) add Canonical Structure resolution to the regular	msozeau
2009-05-10	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-05-09	fix a bug in canonical structures (bug found and fixed by Cyril)	barras
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-24	- New cleaning phase for the entry points of pretyping.ml	herbelin
2009-04-21	fixed CBV strategy: it was too eager on terms like	barras
2009-04-17	- Fix handling of clauses in setoid_rewrite to rewrite under binders	msozeau
2009-04-10	Fix premature optimisation in dependent induction: even variable args need	msozeau
2009-04-09	Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey
2009-04-08	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin