coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-02-06	From v8.2 to trunk:	herbelin
2009-01-23	Really compare evar maps in progress, due to merging in apply and other	msozeau
2009-01-20	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin
2009-01-20	- Fixing bug 1891 (abusive instantiations of evar arguments in	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-17	DISCLAIMER	puech
2009-01-16	Correct a bug in commit 11659	puech
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2009-01-02	Fixed two apparent inconsistencies in matching.ml:	herbelin