| Age | Commit message (Expand) | Author |
| 2007-10-05 | Added the automatic generation of the boolean equality if possible and the | vsiles |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-09-06 | Uniformisation politique de nommage evd/isevars (evd si evar_defs, | herbelin |
| 2007-07-06 | Adding a syntax for "n-ary" rewrite: | letouzey |
| 2007-05-29 | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-17 | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-13 | Proposition de correction pour le bug #1173 (ou du moins pour un | herbelin |
| 2007-03-30 | Changement mineur du comportement de 'rewrite .. in * |-': si le | notin |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2007-03-13 | Correction bug #1439 (comportement de replace by) | notin |
| 2007-02-21 | Correction typo liée au commit 8779 (levait une anomalie) | herbelin |
| 2006-12-22 | remplacement d'un test d'egalite par un test de convertibilite dans injection... | jforest |
| 2006-10-05 | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey |
| 2006-10-03 | Changement de comportement du [rewrite ... in H]: Coq échoue si H | notin |
| 2006-10-03 | Retour sur la suppression du pf_nf (trop d'exemples utilisent avec | herbelin |
| 2006-10-01 | Une passe sur l'injection et la discrimination... | herbelin |
| 2006-09-30 | Suppression de la comparaison (inutile) des paramètres globaux des | herbelin |
| 2006-08-22 | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest |
| 2006-07-05 | Correcting for bug #1167 | jforest |
| 2006-06-12 | Updating documentation of replace and correcting a typo in error message of r... | jforest |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-05-20 | "subst." works now even when it exists an hypothesis have the form "x=x" in t... | jforest |
| 2006-05-02 | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey |
| 2006-05-02 | Changement de comportement de rewrite: face a une egalité setoid, on | letouzey |
| 2006-04-02 | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-01-16 | - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses | herbelin |
| 2005-12-30 | Nettoyage coqlib | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-09-08 | Réparation bug #1004; nettoyage | herbelin |
| 2005-06-06 | essai de typage des instantiations d\'evars | barras |
| 2004-11-21 | Expansion Case dans injection et discriminate (cf bug #829) | herbelin |
| 2004-10-28 | Ajout 'dependent rewrite in' | herbelin |
| 2004-10-27 | Restructuration fonctions de réécriture depuis égalité dépendante; facto... | herbelin |
| 2004-09-30 | New tactic [setoid_]rewrite ... in ... [generate side conditions ...]. | sacerdot |
| 2004-09-30 | Proof term size optimization: setoid_rewrite H where H is an application of | sacerdot |
| 2004-09-29 | New syntax | sacerdot |
| 2004-09-24 | Correction bug report #855 | herbelin |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-12 | inclusion de meta_map dans evar_defs | barras |
| 2004-09-07 | deuxieme vague de modifs: evar_defs fonctionnel | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-07-30 | Protection erreur find_eq_data dans decompEqThen et uniformisation messages d... | herbelin |
| 2004-07-23 | Since setoid_{replace,rewrite} now uses replace there is a circularity | sacerdot |