coq - The formal proof system

Age	Commit message (Expand)	Author
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-28	Raise an error and not an anomaly if a rewrite is attempted on a	msozeau
2009-06-22	Correct treatment of dependent products in signatures: create the evars	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-10	Use the projections for reflexivity, symmetry and transitivity proofs to	msozeau
2009-06-09	Correct handling of the initial existentials from the goal and the ones	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-05-05	Improvements in typeclasses eauto and generalized rewriting:	msozeau
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-21	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau
2009-04-17	- Fix handling of clauses in setoid_rewrite to rewrite under binders	msozeau
2009-04-16	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau
2009-04-14	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau
2009-04-14	Add a combinator for rewriting given a list of terms and fix the	msozeau
2009-04-13	Rewrite of setoid_rewrite to modularize it based on proof-producing	msozeau
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau