coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	iff and impl are now declared as transitive relations.	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	2004-10-06
*	impl is a reflexive relation (it used to be areflexive).	sacerdot	2004-09-29
*	impl relation and impl/and/or/not morphisms over impl declared.	sacerdot	2004-09-29
*	* cleaning/renaming	sacerdot	2004-09-08
*	The Coq part of the reflexive tactic is now able to handle also	sacerdot	2004-09-08
*	* The Coq part of the reflexive tactic setoid_rewrite is generalized to	sacerdot	2004-09-07
*	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot	2004-09-03
*	Zbool déjà dans ZArith_base	herbelin	2004-08-03
*	Minimisation utilisation NNPP	herbelin	2004-08-03
*	Déclaration d'obsolescence	herbelin	2004-08-03
*	Typo	herbelin	2004-08-03
*	Ref	herbelin	2004-08-03
*	Commentaires coqdoc	herbelin	2004-08-01
*	Commentaires coqdoc	herbelin	2004-08-01
*	Nouvelle en-tête	herbelin	2004-07-16
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
*	Nouveaux thms de non circularité de nat	herbelin	2004-06-02
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
*	sumbool et sumor affich avec 'if' si possible	herbelin	2004-04-06
*	Commentaires	herbelin	2004-03-29
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin	2004-03-28
*	MAJ commentaires	herbelin	2004-03-24
*	Definition de la notation de la paire par un motif recursif	herbelin	2004-03-17
*	Commentaires	herbelin	2004-03-17
*	ajout decimal_exp pour interpreter les notations decimales	mohring	2004-03-12
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	MAJ Commentaires	herbelin	2004-02-28
*	Ajout delimiteur pour bool_scope	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	backtrack implicit dans Bvector	marche	2004-02-10
*	patch Bvector: args implicites	marche	2004-02-09
*	MAJ simplification	herbelin	2004-01-27
*	Suppression de Rsyntax en v8	herbelin	2004-01-13
*	bugs avec Pose et Assert	barras	2004-01-09
*	Commentaires en v8	herbelin	2004-01-09
*	Ajout delimiteur et arguments de scope pour list	herbelin	2003-12-24
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
*	Affichage sur le modèle du forall pour le exists	herbelin	2003-12-21
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	power associe a droite	marche	2003-12-05
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	Ratage standardisation Rge_monotony en Rmult_ge_compat_r	herbelin	2003-12-01
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Notation locale pour Rpower	herbelin	2003-11-29
*	Ajout lemmes, simplification preuve de SeqProp	herbelin	2003-11-29
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29