coq - The formal proof system

Age	Commit message (Expand)	Author
2004-10-19	Proof term size reduction (again).	sacerdot
2004-10-18	* Code simplification and clean-up. In particular there is no more code	sacerdot
2004-10-11	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin
2004-10-07	iff and impl are now declared as transitive relations.	sacerdot
2004-10-06	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot
2004-10-06	added transitivity	barras
2004-09-29	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-08	* cleaning/renaming	sacerdot
2004-09-08	The Coq part of the reflexive tactic is now able to handle also	sacerdot
2004-09-07	* The Coq part of the reflexive tactic setoid_rewrite is generalized to	sacerdot
2004-09-03	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot
2004-08-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-01	Commentaires coqdoc	herbelin
2004-08-01	Commentaires coqdoc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-06-25	simplified proof (eq and eqT are now the same)	barras
2004-06-02	Nouveaux thms de non circularité de nat	herbelin
2004-06-02	eq2eqT et eqT2eq devenus obsolètes	herbelin
2004-04-06	sumbool et sumor affich avec 'if' si possible	herbelin
2004-03-29	Commentaires	herbelin
2004-03-28	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin
2004-03-24	MAJ commentaires	herbelin
2004-03-17	Definition de la notation de la paire par un motif recursif	herbelin
2004-03-17	Commentaires	herbelin
2004-03-12	ajout decimal_exp pour interpreter les notations decimales	mohring
2004-03-03	ide: silent behavior better, save icon, -byte works	marche
2004-02-28	MAJ Commentaires	herbelin
2004-02-12	Ajout delimiteur pour bool_scope	herbelin
2004-02-12	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin
2004-02-10	backtrack implicit dans Bvector	marche
2004-02-09	patch Bvector: args implicites	marche
2004-01-27	MAJ simplification	herbelin
2004-01-13	Suppression de Rsyntax en v8	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2004-01-09	Commentaires en v8	herbelin
2003-12-24	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-23	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin
2003-12-21	Affichage sur le modèle du forall pour le exists	herbelin
2003-12-16	Duplication temporaire des règles de syntaxe des paires	herbelin
2003-12-15	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras
2003-12-05	power associe a droite	marche
2003-12-04	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin
2003-12-01	Ratage standardisation Rge_monotony en Rmult_ge_compat_r	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin