| Age | Commit message (Expand) | Author |
| 2006-03-04 | Titres moins envahissants pour coqdoc | herbelin |
| 2006-02-27 | quelques raccourcis commodes + un f_equal plus efficace | letouzey |
| 2006-02-23 | Ajout 'exists! x:A, P (suite) | herbelin |
| 2006-02-23 | Ajout 'exists! x:A, P | herbelin |
| 2006-02-10 | code mort | herbelin |
| 2006-02-06 | Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru... | herbelin |
| 2006-01-22 | Application de la suggestion de Nicolas Magaud (#1060) | herbelin |
| 2006-01-21 | Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es... | herbelin |
| 2006-01-21 | Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc | herbelin |
| 2006-01-19 | Correction associativité de IF et exists (visible à l'affichage uniquement ... | herbelin |
| 2005-12-22 | Contrepartie de la suppression des boites automatiques dans format | herbelin |
| 2005-11-30 | changement parametres inductifs dans les theories | mohring |
| 2005-08-26 | *** empty log message *** | letouzey |
| 2005-05-19 | Documentation | herbelin |
| 2005-05-17 | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin |
| 2005-03-31 | Added option_map | herbelin |
| 2005-02-23 | quelques tactics ltac | letouzey |
| 2005-02-04 | Essai d'utilisation de 'where' pour les notations | herbelin |
| 2005-02-03 | Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs | herbelin |
| 2005-02-03 | Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs | herbelin |
| 2004-12-06 | Inutile de réserver les notations à base de '{ }' | herbelin |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-08-01 | Commentaires coqdoc | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-04-06 | sumbool et sumor affich avec 'if' si possible | herbelin |
| 2004-03-29 | Commentaires | herbelin |
| 2004-03-17 | Definition de la notation de la paire par un motif recursif | herbelin |
| 2004-02-28 | MAJ Commentaires | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2004-01-09 | Commentaires en v8 | herbelin |
| 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-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-21 | Tri et typo | herbelin |
| 2003-11-14 | Automatisation de la traduction de iff_trans; renommage IF | herbelin |
| 2003-11-14 | Backtrack sur Peano | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-12 | Ajout lemme projections | herbelin |
| 2003-11-12 | %type au lieu de %T | herbelin |
| 2003-11-12 | Lemmes dans un sens plus naturel | herbelin |
| 2003-11-12 | petits changements de syntaxe | barras |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
| 2003-10-28 | Ordre (symbolique) des Require | herbelin |
| 2003-10-28 | Passage de la notations de paire dans core_scope | herbelin |
| 2003-10-28 | Passage des notations de type dans type_scope | herbelin |
| 2003-10-28 | Ajout %core; MAJ niveau connecteurs logique | herbelin |