coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	Fix lifting of constraints in generalized rewriting tactic.	msozeau	2010-03-07
*	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau	2010-03-06
*	Improvements in generalized rewriting:	msozeau	2010-03-05
*	Support for generalized rewriting under dependent binders, using the	msozeau	2010-01-26
*	Fix "Existing Instance" to handle globality information and "Existing	msozeau	2009-12-27
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin	2009-12-13
*	Fix anomaly when using typeclass resolution with filtered hyps in evars.	msozeau	2009-12-06
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Correctly do backtracking during type class resolution even if only new	msozeau	2009-10-05
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Allow setoid rewrite to rewrite in pattern-matching scrutinees or	msozeau	2009-09-09
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Support globality flag properly for "Add Morphism foo : foo_mor" syntax.	msozeau	2009-09-03
*	Stop unnecessary use of lazy values for constraints, simplifying	msozeau	2009-09-02
*	- 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