aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Collapse)Author
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ↵herbelin
ajout FreshId git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4073 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ↵herbelin
inefficacité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4063 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4005 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Bug: lookup inapproprie dans subst_tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3921 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Relachement globalisation Unfold en usage interactifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Trop de restriction pour les TacDefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3899 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Prise en compte des variables de grammaires de tactiques et dédollarisation ↵herbelin
des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTac; localisation des appels à des tactiques ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Correction d'un bug introduit dans le backtracking d'occurrencedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3677 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Chargement dynamique de .cmadelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Debugger plus informatifdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Mauvais environnement d'évaluation pour les globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3597 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3566 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Mauvaise interprétatin de IdentArgTypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3550 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Protection contre les noms de tactiques inconnus; restriction exceptions ↵herbelin
rattrapées dans les Match git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3546 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Petits bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3540 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Utilisation d'une exception 'catchable'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3535 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3529 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Traitement spécial pour les types à l'internalisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3443 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Ajout du vernac Proof withgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Re-ajout constrInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16correction de bugs:barras
- subst_term_gen ne depliait pas les constantes locales de maniere uniforme - la tactique Simpl ne simplifiait pas les constantes definies dans le contexte de but - la conversion d'un constr vers identificateur ne prenait pas en compte les inductifs et constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Bug dans la globalisation des arguments de tactiques primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2882 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2853 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2779 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2743 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:13:49 +0000