coq - the Coq proof assistant

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