coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	impl relation and impl/and/or/not morphisms over impl declared.	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
*	Test updated.	sacerdot	2004-09-29
*	Hugly temporary notation	sacerdot	2004-09-29
*	The quoting function is now 100% complete.	sacerdot	2004-09-29
*	maj	filliatr	2004-09-28
*	maj	filliatr	2004-09-28
*	The quoting function is now almost complete (in the sense that it can find	sacerdot	2004-09-28
*	maj	filliatr	2004-09-27
*	The quoting function of the reflexive tactic is now sound: all the terms	sacerdot	2004-09-27
*	?(mod_delta=true) parameter added to each unification function.	sacerdot	2004-09-27
*	firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...	corbinea	2004-09-27
*	corrected bug when lhs is matched w.r.t delta	barras	2004-09-27
*	collapse apps of patterns to avoid failures	barras	2004-09-27
*	maj	filliatr	2004-09-26
*	no-assert en mode natif	herbelin	2004-09-26
*	Ajouts	herbelin	2004-09-25
*	Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...	herbelin	2004-09-25
*	- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient	herbelin	2004-09-25
*	maj	filliatr	2004-09-24
*	maj	filliatr	2004-09-24
*	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot	2004-09-24
*	Ajout bug #255	herbelin	2004-09-24
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	Correction bug report #855	herbelin	2004-09-24
*	maj	filliatr	2004-09-23
*	error if binder was already defined	barras	2004-09-23
*	maj	filliatr	2004-09-22
*	maj	filliatr	2004-09-22
*	link order again	barras	2004-09-22
*	maj	filliatr	2004-09-21
*	maj	filliatr	2004-09-20
*	pbs with link order and deps	barras	2004-09-20
*	maj	filliatr	2004-09-19
*	maj	filliatr	2004-09-17
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	repaired deps	barras	2004-09-17
*	maj	filliatr	2004-09-16
*	maj	filliatr	2004-09-15
*	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
*	maj	filliatr	2004-09-14
*	maj	filliatr	2004-09-14
*	evar tactic bugfix	corbinea	2004-09-14
*	maj	filliatr	2004-09-13
*	* 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
*	maj	filliatr	2004-09-12
*	maj	filliatr	2004-09-12