aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Collapse)AuthorAge
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
| | | | | | | | | | | | | | This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
* pushed evar reduction in kernelGravatar barras2009-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved simplGravatar barras2008-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
* another bug with simplGravatar barras2008-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug 1791: simpl was performing eta expansionGravatar barras2008-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
| | | | | | | | | | | | | | | - Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
* refined the conversion oracleGravatar barras2008-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1835 + correction bug occur-check résultant en unGravatar herbelin2008-04-18
| | | | | | | | | | | | "cannot define an evar twice" --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M tacred.ml M evarutil.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10815 85f007b7-540e-0410-9357-904b9bb8a0f7
* fold travaille maintenant sur la forme beta-iota-zeta réduite duGravatar herbelin2008-03-10
| | | | | | | | | corps de la constante (comme unfold le fait ici), de telle sorte que "unfold f; fold f" marche (cf bug 1789) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit complément au commit 10131.Gravatar herbelin2007-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10136 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
| | | | | | | | | | | | | | | | | | | | the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection d'un warning par if_verboseGravatar herbelin2007-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,Gravatar herbelin2007-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | reduce_to_ind et reduce_to_ref a révélé que ceux-ci pouvaient contourner l'opacité des constantes lorsque celles-ci apparaissaient comme argument d'un match ou d'un fix (et ce depuis la V5.10 environ). Exemple: Definition f (A B:Set) := pair A B. Opaque f. Goal fst (f unit unit) -> True. intro H. destruct H. (* bypassed opacity *) Definition f (A:Set) := A. Opaque f. Goal (f unit) -> True. intro H. destruct H. (* didn't bypass opacity *) Contourner le statut Opaque quand on recherche un inductif (ce qui est le rôle de reduce_to_ind) ne paraît pas problématique (et il se trouve d'ailleurs que CoRN/ftc/TaylorLemma.v en profitait). Ce contournement de l'opacité a donc été généralisé au cas de constantes arrivant en tête sans être argument d'un match ou d'un fix. Contourner le statut Opaque quand on recherche une constante particulière (ce qui est le rôle général de reduce_to_ref qui est maintenant le seul à reposer sur one_step_reduce) paraît en revanche plus douteux. Plus de contournement d'opacité pour reduce_to_ref donc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1491Gravatar herbelin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9761 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
* amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)Gravatar barras2006-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
| | | | | | | prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug invert_names (cf bug #1031)Gravatar herbelin2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵Gravatar herbelin2005-05-20
| | | | | | reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵Gravatar herbelin2005-01-02
| | | | | | dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵Gravatar herbelin2004-12-29
| | | | | | convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
* UserError in reduce_to_*_refGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6382 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification de la typability de 'pattern'Gravatar herbelin2004-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵Gravatar herbelin2004-09-08
| | | | | | incorrects: 0 au lieu de 1 et lv dans le mauvait sens) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6075 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de suppression de eta dans simpl (cf bug #779)Gravatar herbelin2004-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Terminologie plus intuitive: evaluable -> unfoldableGravatar herbelin2004-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #606: mis un message d'erreur plus clairGravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (suite)Gravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (2 protections ↵Gravatar herbelin2004-02-13
| | | | | | maintenant !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵Gravatar herbelin2004-01-27
| | | | | | paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage opaqueGravatar herbelin2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'Gravatar herbelin2003-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Simpl f'Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout reduce_to_quantified_refGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 07:40:12 +0000