| Age | Commit message (Expand) | Author |
| 2006-09-23 | Correction bug #1229 (toplevel "unresolved evar" fled through | herbelin |
| 2006-09-22 | Ajout d'une valeur VList dans tacinterp pour permettre de cabler des | herbelin |
| 2006-09-21 | Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s... | herbelin |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-09-12 | Indentation + svnprop | notin |
| 2006-09-01 | Correction bug d'ordonnancement des hyps d'induction dans induction/destruct | herbelin |
| 2006-08-28 | improve the amount of information given by the Ltac tactic debugger | bertot |
| 2006-08-23 | Bug in replace tactics introduced in r9073 (overlap between replace .. with a... | jforest |
| 2006-08-22 | Forgot a file in previous commit | jforest |
| 2006-08-22 | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest |
| 2006-08-17 | corrects an error in the substitution of module paths inside tactics: | bertot |
| 2006-07-28 | Reparation bug Show intros: les hypothèses introduites précédemment | courtieu |
| 2006-07-20 | Correction du bug #1116 | jforest |
| 2006-07-18 | amelioration du comportement de induction (retour a la version V8.0) | jforest |
| 2006-07-05 | Correcting for bug #1167 | jforest |
| 2006-06-27 | Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'... | herbelin |
| 2006-06-23 | Suite utilisation hyp au lieu ident: donne la localisationn | herbelin |
| 2006-06-23 | Correction ident -> hyp pour dinterpréter des identificateurs devant êt... | herbelin |
| 2006-06-23 | Préservation compatibilité interprétation quantified hypothesis (provisoir... | herbelin |
| 2006-06-22 | Nettoyage, uniformisation | herbelin |
| 2006-06-21 | Harmonisation de l'interprétation des intropattern | herbelin |
| 2006-06-19 | bug serieux efficacite de ltac | barras |
| 2006-06-12 | Updating documentation of replace and correcting a typo in error message of r... | jforest |
| 2006-06-08 | Changement du type d'argument 'TacticArgType X' en un type | herbelin |
| 2006-06-06 | reparation pour le bug #1072 (soufflee par J. Forest): | letouzey |
| 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-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-05-20 | "subst." works now even when it exists an hypothesis have the form "x=x" in t... | jforest |
| 2006-05-05 | encore un correctif sur le rewrite H in setoid: | letouzey |
| 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-05-02 | Correction bug du correctif bug assert as | herbelin |
| 2006-05-02 | Bug assert as | herbelin |
| 2006-04-28 | Standardisation du nom des méthodes de Evd | herbelin |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-26 | Diverses corrections de l'afficheur et du traducteur pour s'assurer de | herbelin |
| 2006-04-12 | induction on multiple arguments made better: | courtieu |
| 2006-04-11 | adding a new tactic [intro_avoiding idl] which acts as intro but prevents the | jforest |
| 2006-04-06 | Enlevement de message d'erreur garbage. | courtieu |
| 2006-04-05 | resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses | letouzey |
| 2006-04-05 | ajout d'un rattrapage d'erreur pour "induction using". | courtieu |
| 2006-04-02 | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-03-22 | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | herbelin |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-03-12 | -Debugging multiple induction, a bug appeared when having function | courtieu |
| 2006-03-05 | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin |
| 2006-03-02 | Correction bug #1097 (dû à une typo...) | herbelin |