aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2007-02-06Report de la révision 9599 de la v8.1 dans le trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9600 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Suppression de code mortnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29bugfix for suffices (support for open head)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9555 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29finalized sufficescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9552 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-28"suffices" implemented + syntax cleanupcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-25decl mode: anonymous factscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22Correction du bug #1315:notin
- ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22changes in declarative language : by term using tacticcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-26Report correction bug #1289 dans trunk (r9435 pour branche v8.1)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans ↵jforest
injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13Dépliage du terme d'induction avant suppression quand celui-ci est unherbelin
terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf success/destruct.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9447 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Correction bug #1041 (double cause : non évitement des noms existants enherbelin
cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-11Changement dans le kernel : bgregoir
- essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
degrés de liberté concernant les instances de méta (cumulativité et possibilité d'éta-expansion) de telle sorte que la fusion d'équations se fasse modulo ces degrés de liberté. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Ajout de dépliage de l'énoncé, si besoin est, dans apply inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9363 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Correction d'un bug refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9359 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-01Quick hack to solve to complexity issue in function mark_occurherbelin
(but should probably not work in presence of morphisms to Leibniz's equality). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9331 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Retour sur la modification apportée en r9289, et nouvelle correction du bug ↵notin
#1259 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9328 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27simplif de la partie ML de ring/fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Affichage d'un message d'erreur losque qu'une relation n'a pas été ↵notin
déclarée (Setoid_replace.find_relation_class) (ferme le bug #1259) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9289 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Petit bug apply inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9281 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-25Correction d'une tentative incorrecte (révision 9266) de clarificationherbelin
du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle correction qui évite ce codage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Insère une coercion vers Sortclass dans 'contradiction' si nécessaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9269 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Extension de la primitive ltac fresh pour qu'elle accepte une liste deherbelin
noms et de chaînes qu'elle va concaténer pour créer un nom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9267 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Ajout de la tactique "apply in".herbelin
Au passage, déplacement des tactiques cut and co plus en amont + commentaires. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9266 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Interprétation du terme comme type dans 'change' si pas de 'with' (pour ↵herbelin
bénéficier des coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9264 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23Fixed "Show intros" which did not look at hypothesis.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9260 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Correction du bug #1255 (réécriture setoid sous un produit)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9253 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16affichage des ... dans les scriptsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-03Changement de comportement du [rewrite ... in H]: Coq échoue si Hnotin
apparaît dans le but ou dans l'une des hypothèses (ferme les bugs #447, #883 et #1228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-03Retour sur la suppression du pf_nf (trop d'exemples utilisent avecherbelin
profit la simplification des arguments -- même si dans quelques cas trop de réduction obligent à revenir en arrière). Remplacement par un hack rapide (et non "scalable"). Suppression code mort oublié commit précédent sur equality.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9199 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-01Une passe sur l'injection et la discrimination...herbelin
Efficacité: - remplacement du typage par du re-typage léger - suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?] - remplacement des tests aveugles de projection impossible par un test qui vérifie au fur et à mesure que les filtrages sont autorisés Réorganisation: - factorisation des parties communes de injEq/discrEq/decompEq (à noter l'ordre inverse de génération des équations dans inj et decomp...) - uniformisation des noms "e" et "ee" utilisés dans la construction des combinateurs de discrimination Extension: - ajout d'une clause "as" à injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-30Suppression de la comparaison (inutile) des paramètres globaux desherbelin
constructeurs dans la recherche des positions de divergence entre expressions construites (possible source d'inefficacité d'injection/discriminate dans le cas de paramètres globaux convertibles mais syntaxiquement distincts -- cf rapport de bug 1173, première suggestion, même si dans le cas soumis les paramètres sont syntaxiquement les mêmes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9193 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26fixed error mesg in decl modecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9177 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-25 Permet a un unfold de recevoir ses occurences a travers une variable Ltac.letouzey
P.ex: Tactic Notation "test" integer(i) := unfold plus at i Ou meme: Tactic Notation "test" ne_integer_list(i) := unfold plus at i (voir commit 9159 d'Hugo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9175 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23Correction bug #1229 (toplevel "unresolved evar" fled throughherbelin
Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-21Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter ↵herbelin
sans ouverture, comme c'est le cas pour les autres Hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9157 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-12Indentation + svnpropnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Correction bug d'ordonnancement des hyps d'induction dans induction/destructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9119 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28improve the amount of information given by the Ltac tactic debuggerbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with ↵jforest
and replace_term). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9076 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22Forgot a file in previous commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9074 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17corrects an error in the substitution of module paths inside tactics:bertot
objects of the form TacDynamic should not be left unchanged if their content is tagged with "constr". This correction makes that setoid ring can now work with rings that were declared inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Reparation bug Show intros: les hypothèses introduites précédemmentcourtieu
dans le même paquet doivent être typables pour décider le nom des suivantes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9061 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 22:45:41 +0000