aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
| | | | | | | evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1634 + ajout de bugs dans la test-suiteGravatar notin2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1322Gravatar notin2007-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
| | | | | | | | | modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new tactic to generalize an instantiated inductive predicate adding ↵Gravatar msozeau2007-08-07
| | | | | | equalities. Useful to do so-called "ford" induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
| | | | | | | | Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement de interp_ident pour que l'ident interprété soit au choixGravatar herbelin2007-07-18
| | | | | | | | frais (par exemple pour "intro") ou pas forcément (par exemple pour "fresh") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
| | | | | | | | | utilities from Util. Some additions in Util, and simplifications in various files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
| | | | | | | | | | | | | | | | | | | | | | rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
| | | | | | | | rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
* killing some more non-exhaustive patternsGravatar letouzey2007-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
| | | | | | | | | (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
| | | | | | | | métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour à un message d'erreur d'apply qui montre un échec sans sans réduction Gravatar herbelin2007-05-28
| | | | | | | | de la conclusion du lemme git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9865 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fix for bug #1397: Gravatar letouzey2007-05-23
| | | | | | | | | | | | | | | | | | | | | | | setoid_reflexivity may discover it is doing plain Leibniz stuff (see exception Optimize in setoid_replace), and falls back to the usual reflexivity. Except that this one, due to the lack of delta-red, refuses to handle the job, and gives it back to setoid_reflexivity: a loop is born. quick fix for the moment: add some whd_betadeltaiota to reflexivity in the special situation where reflexivity is called back by setoid_reflexivity. Similar issue & fix for symmetry, transitivity. rewrite has potentially the same problem, but I can't manage to trigger a wild loop in practice. This code clearly deserves a closer look someday... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | apply afin de reculer au plus tard les décisions irréversibles et en particulier de pouvoir typer les with-bindings modulo coercions : - l'unification des types des métas données en with-bindings est retardé à après l'unification (unify_0) de telle sorte que les instances trouvées par unify_0 soient prioritaires et que la décision d'insérer éventuellement des coercions autour des valeurs données en with-bindings se fasse au dernier moment; - toujours pour permettre d'insérer ultimement des coercions, l'instantiation des with-bindings ne se fait plus l'appel unify_0 (cf clenv_unique_resolver); - pour permettre ce retardement sans limiter le test de conversion que unify_0 fait sur les termes clos, on transmet à unify_0 les métas données en with-bindings (ainsi l'instantiation de ces métas peut être faite dynamiquement au moment du test de clôture); - parce que les métas données en with-bindings qui sont en position de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent simplifier le problème d'unification (et elles ne sont pas de toutes façons pas réinférables au premier ordre), on continue à les substituer avant l'appel à unify_0 (cf meta_reducible_instance); - pour l'unification du second-ordre, on continue d'instancier les with-bindings et d'unifier les types des with-bindings avant unification; - reste à régler un problème de compatibilité lorsque le résultat de l'unification des types des with-bindings est utilisé pour rendre un terme clos et pour permettre à unify_0 d'utiliser la conversion. + meilleure compatibilité de apply, split, left, right pour le code qui l'utilise avec des bindings clos + nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur l'effacement dans le contexte de but des lieursGravatar herbelin2007-05-19
| | | | | | | | | | | apparaissant sans nom dans "refine" (quelques incompatibilités, par exemple dans les preuves de Lannion/continuations/Nxaccu_ex.core_V1, Bordeaux/Additions/log2_spec.ceiling_log2, et Bordeaux/NewSearchTree/search_tree.rm). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interprétation des listes de VarArgType dans les notations faisantGravatar herbelin2007-05-18
| | | | | | | | référence à des arguments génériques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wish #1582 (3eme)Gravatar herbelin2007-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)Gravatar herbelin2007-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques essais autour du wish implicite au rapport de bug #1582Gravatar herbelin2007-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9836 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bug dans Function et augmentation de la classe des fonctions ↵Gravatar jforest2007-05-17
| | | | | | supportees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction des bugs #1537 (anomalie sur signature incomplète) et #1536Gravatar herbelin2007-05-17
| | | | | | | | (anomalie sur types non convertibles) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9830 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
| | | | | | | | | par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7. unfold "+". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
| | | | | | | | | Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed glitch in escapeGravatar corbinea2007-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9800 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin des conclusions multiplesGravatar corbinea2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug plus poussé induction dépendanteGravatar corbinea2007-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9787 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
| | | | | | | | | | | (les let-in étaient comptés comme des produits, introduisant une incohérence sur le nombre de produits à instancier dans les lemmes appelés par apply). - Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition. - Doc développeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de simplest_eapply, utilisé dans la contrib interfaceGravatar notin2007-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9776 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix bug with dependent inductive familiesGravatar corbinea2007-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
| | | | | | | | | | de la réduction paresseuse du lemme [eapply n'en profitait pas], et l'un et l'autre profite de l'unification2nd ordre sur la forme réduite du lemme [apply n'en profitait pas]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de partage de code entre apply et eapplyGravatar herbelin2007-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proposition de correction pour le bug #1173 (ou du moins pour unGravatar herbelin2007-04-13
| | | | | | | | | | exemple de divergence soumis par Andrew Appel) [on renonce à normaliser pour trouver l'ensemble minimal de variables liées dans le 2e membre d'une égalité dépendante] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
| | | | | | | | | | | | | | | | | | | | | | | fix/cofix avec réutilisation du nom de la constante dans les appels récursifs), avec notamment uniformisation des comportements et des noms de fonctions de réduction. En particulier, on a les changements sémantiques suivants : - léger changement de simpl: si appliqué à un fix explicite, il sait réduire l'argument en un constructeur comme si le fix était caché derrière une constante (cf exemple dans test-suite/output/reduction.v); - léger changement de hnf: si appliqué à un match ou un fix explicite et que l'argument de ce match ou de ce fix nécessite un calcul impliquant des constantes récursives, il sait conserver les noms (à la manière de simpl) comme il sait déjà le faire si ce match ou ce fix était caché derrière une constante (cf exemple dans test-suite/output/reduction.v); - changement similaire de one_step_reduce utilisé dans reduce_to_*_ref (difficile d'imaginer les effets mais sans doute très peu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension to the general sequence operator (tactical). Now in addition to ↵Gravatar emakarov2007-04-02
| | | | | | | | | | | the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement mineur du comportement de 'rewrite .. in * |-': si leGravatar notin2007-03-30
| | | | | | | | | | constr avec lequel on réécrit contient une hypothèse H, on ne réécrit pas dans H (corrige le bug #1446) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a parameter to QuestionMark evar kind to say it can be turned into an ↵Gravatar msozeau2007-03-19
| | | | | | | | | | obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1439 (comportement de replace by)Gravatar notin2007-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les warnings (ajout Options.warn déclenchée par ↵Gravatar herbelin2007-02-24
| | | | | | | | | compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeGravatar herbelin2007-02-22
| | | | | | | | "R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au au lieu de w_unify (suggestion de GG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction typo liée au commit 8779 (levait une anomalie)Gravatar herbelin2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9666 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation absence d'interprétation des liaisons vers listesGravatar herbelin2007-02-15
| | | | | | | d'occurrences (clause "at") dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:13:12 +0000