| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2006-02-23 | trying to fix a bug in pazrameter order in the multiple induction | coq |
| 2006-02-17 | cleaning | coq |
| 2006-02-17 | bug correction in the decomposition of an induction scheme. | coq |
| 2006-02-17 | changed the decomposition of an induction scheme | coq |
| 2006-02-16 | added isProd to term.mli. | coq |
| 2006-02-15 | continuing the generalization of "induction". Now induction schemes | coq |
| 2006-02-10 | induction now admits multiple induction arguments. The principle must | coq |
| 2006-02-05 | Debugging en syntaxe v8 | herbelin |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2006-01-28 | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin |
| 2006-01-28 | Suppression code pour hints nommés à la V7 (voire à la V6...) | herbelin |
| 2006-01-24 | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2006-01-21 | Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f... | herbelin |
| 2006-01-21 | Backtrack commit précédent (incompatible avec le choix de prendre Idtac com... | herbelin |
| 2006-01-20 | Ajout de la contrainte de résoudre l'assertion dans 'assert by' | herbelin |
| 2006-01-19 | Conséquences supplémentaires de la fin du support v7 | herbelin |
| 2006-01-19 | Export eassumption | herbelin |
| 2006-01-16 | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq | herbelin |
| 2006-01-16 | Code redondant | herbelin |
| 2006-01-16 | - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses | herbelin |
| 2006-01-11 | Standardisation du nom de subst_raw en subst_rawconstr | herbelin |
| 2006-01-11 | Standardisation du nom de subst_raw en subst_rawconstr | herbelin |
| 2006-01-11 | Résidus du traducteur v7 -> v8 | herbelin |
