| Commit message (Expand) | Author | Age |
|---|
| * | improve the amount of information given by the Ltac tactic debugger |  bertot | 2006-08-28 |
| * | Bug in replace tactics introduced in r9073 (overlap between replace .. with a... |  jforest | 2006-08-23 |
| * | 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-22 |
| * | corrects an error in the substitution of module paths inside tactics: | bertot | 2006-08-17 |
| * | Reparation bug Show intros: les hypothèses introduites précédemment |  courtieu | 2006-07-28 |
| * | Correction du bug #1116 | jforest | 2006-07-20 |
| * | amelioration du comportement de induction (retour a la version V8.0) | jforest | 2006-07-18 |
| * | Correcting for bug #1167 | jforest | 2006-07-05 |
| * | Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'... |  herbelin | 2006-06-27 |
| * | 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-23 |
| * | Nettoyage, uniformisation | herbelin | 2006-06-22 |
| * | Harmonisation de l'interprétation des intropattern | herbelin | 2006-06-21 |
| * | bug serieux efficacite de ltac |  barras | 2006-06-19 |
| * | Updating documentation of replace and correcting a typo in error message of r... | jforest | 2006-06-12 |
| * | Changement du type d'argument 'TacticArgType X' en un type | herbelin | 2006-06-08 |
| * | reparation pour le bug #1072 (soufflee par J. Forest): |  letouzey | 2006-06-06 |
| * | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
| * | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
| * | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
| * | "subst." works now even when it exists an hypothesis have the form "x=x" in t... | jforest | 2006-05-20 |
| * | encore un correctif sur le rewrite H in setoid: | letouzey | 2006-05-05 |
| * | 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-05-02 |
| * | 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-28 |
| * | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
| * | Diverses corrections de l'afficheur et du traducteur pour s'assurer de | herbelin | 2006-04-26 |
| * | induction on multiple arguments made better: | courtieu | 2006-04-12 |
| * | adding a new tactic [intro_avoiding idl] which acts as intro but prevents the | jforest | 2006-04-11 |
| * | Enlevement de message d'erreur garbage. | courtieu | 2006-04-06 |
| * | 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-05 |
| * | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin | 2006-04-02 |
| * | 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-22 |
| * | + destruct now works as induction on multiple arguments : | jforest | 2006-03-21 |
| * | -Debugging multiple induction, a bug appeared when having function | courtieu | 2006-03-12 |
| * | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin | 2006-03-05 |
| * | Correction bug #1097 (dû à une typo...) | herbelin | 2006-03-02 |
| * | trying to fix a bug in pazrameter order in the multiple induction |  coq | 2006-02-23 |
| * | 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-17 |
| * | added isProd to term.mli. | coq | 2006-02-16 |
| * | continuing the generalization of "induction". Now induction schemes | coq | 2006-02-15 |
bertot
jforest
courtieu
herbelin
barras
letouzey
notin
msozeau
coq