| Age | Commit message (Expand) | Author |
| 2007-01-02 | Add f_equal case for 6 arguments. | msozeau |
| 2006-10-24 | Ajout de la tactique 'remember' | herbelin |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-10-05 | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey |
| 2006-09-22 | Ajout d'une valeur VList dans tacinterp pour permettre de cabler des | herbelin |
| 2006-09-21 | incomplete and temporary fix for PR#1222: revert accepts up to 10 args | letouzey |
| 2006-08-28 | Passage à une définition de inhabited plus dans les 'standard mathématique... | herbelin |
| 2006-06-25 | repetition d'hypotheses dans well_founded_induction_type_2 | letouzey |
| 2006-06-09 | Modification déf de exists! pour éviter une éta-expansion et pouvoir être... | herbelin |
| 2006-06-04 | Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit... | herbelin |
| 2006-06-04 | Ajout exists! et restructuration/extension des fichiers sur la | herbelin |
| 2006-05-29 | Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiés | herbelin |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-03-17 | Modification des propriétés (svn:executable) | notin |
| 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 |