coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	setoid_symmetry in ... implemented.	sacerdot	2004-10-07
*	New commands	sacerdot	2004-10-07
*	Now Print Setoids prints also the transitivity justification of transitive	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	2004-10-06
*	Add Setoid now accepts also quantified setoids.	sacerdot	2004-10-06
*	* code clean up	sacerdot	2004-10-06
*	Th unification procedure has been made a bit more complete by recording the	sacerdot	2004-10-06
*	Leibniz equality is now a quantified relation.	sacerdot	2004-10-06
*	* code simplification	sacerdot	2004-10-05
*	* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whether	sacerdot	2004-10-05
*	* Bug fix: in case of non dependent implications the second argument was	sacerdot	2004-10-05
*	eq_constr replaced with a conversion test where possible.	sacerdot	2004-10-01
*	1. added new parameter "as ..." to Add Setoid. Used to synthesize the name	sacerdot	2004-10-01
*	add_setoid has a new parameter used to synthesize the morphism name.	sacerdot	2004-10-01
*	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot	2004-10-01
*	New tactic	sacerdot	2004-09-30
*	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	sacerdot	2004-09-30
*	Proof term size optimization: setoid_rewrite H where H is an application of	sacerdot	2004-09-30
*	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot	2004-09-30
*	setoid_replace E1 with E2	sacerdot	2004-09-30
*	* error messages improved	sacerdot	2004-09-29
*	Add Relation is now able to detect non well typed relation registrations.	sacerdot	2004-09-29
*	The Add Morphism command is now able to detect in advance:	sacerdot	2004-09-29
*	New syntax	sacerdot	2004-09-29
*	The Prod special case works only when the premise is of type Prop.	sacerdot	2004-09-29
*	1. major code clean-up for the Prod case	sacerdot	2004-09-29
*	impl is a reflexive relation (it used to be areflexive).	sacerdot	2004-09-29
*	1) bug fixed: new goals where compared according to the relation arguments	sacerdot	2004-09-29
*	The list of possible solutions proposed by the tactic cannot contain any	sacerdot	2004-09-29
*	Hugly temporary notation	sacerdot	2004-09-29
*	The quoting function is now 100% complete.	sacerdot	2004-09-29
*	The quoting function is now almost complete (in the sense that it can find	sacerdot	2004-09-28
*	The quoting function of the reflexive tactic is now sound: all the terms	sacerdot	2004-09-27
*	corrected bug when lhs is matched w.r.t delta	barras	2004-09-27
*	- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient	herbelin	2004-09-25
*	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot	2004-09-24
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	Correction bug report #855	herbelin	2004-09-24
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	put empty_env in hint clause (vo were becoming huge!)	barras	2004-09-15
*	evar tactic bugfix	corbinea	2004-09-14
*	* The ML tactic is now also aware of rewriting directions.	sacerdot	2004-09-13
*	The ML part of the tactic now knows about covariant and contravariant morphism	sacerdot	2004-09-13
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	simplification de clenv	barras	2004-09-10
*	Dead code removed.	sacerdot	2004-09-10
*	1. add_new_morphism now has a new optional argument that is the signature	sacerdot	2004-09-10
*	add_new_morphism has now a new argument that is the signature	sacerdot	2004-09-10