aboutsummaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
AgeCommit message (Collapse)Author
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵herbelin
aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-15Allow auto to have a parametric argument (wish #967)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵herbelin
statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6678 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification ↵herbelin
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵herbelin
tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵herbelin
evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28more evar stuffcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27Bug affichage ClearBodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5771 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵herbelin
VERNAC EXTEND (e.g. Hint Rewrite) [2eme] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5526 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵herbelin
VERNAC EXTEND (e.g. Hint Rewrite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5525 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour ↵herbelin
paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵herbelin
variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵herbelin
des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09bugs avec Pose et Assertbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24Bug affichage Decomposeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5144 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-17ajout test de non-regression Clear d'une def localebarras
reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-01Nouvelle tactique EExistsclrenard
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments ↵herbelin
recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la ↵herbelin
bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Idtac peut prendre un argument à affichernarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4775 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Traduction des noms pour les refs de pr_glob_generic (via pr_global)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4760 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵herbelin
par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Traduction des idents aussi dans le printer generique des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4664 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cablage en dur de inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16En attendant l'afficheur...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4405 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4331 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4311 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4310 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24Ajout FreshIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 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-04-29Factorisation des produits de même type; parenthèses autour des x:=c et ↵herbelin
n:=c dans les 'with bindings'; mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3975 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-27Reparation affichage LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3958 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:55:04 +0000