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