coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-04-08	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin
2009-04-03	Fix obvious bug in evars_of_named_context.	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-28	Fix bug #2056 (discharge bug).	msozeau
2009-03-22	Compromise wrt introduction-names compatibility issue after addition	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-20	On passe les last_mods (un des champs de Evd.evar_defs) de list	aspiwack
2009-02-20	On ne met plus rien dans les last_mods tant que conv_pbs est vide.	aspiwack
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-09	memoized is_ground_env	barras
2009-02-06	pushed evar reduction in kernel	barras