aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_ltac.ml4
AgeCommit message (Expand)Author
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-08-05Correction de bugs:herbelin
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-01Clarification de l'ordre d'interprétation des variables dans ltac. Enherbelin
2008-04-29Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laherbelin
2008-04-14Diverses corrections herbelin
2008-02-10suppression code mort oublié lors du commit 10495herbelin
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-04-02Extension to the general sequence operator (tactical). Now in addition to ...emakarov
2007-02-15Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsherbelin
2006-11-02gestion speciale du niveau 5 des ltacbarras
2006-10-31syntaxe du let in encorebarras
2006-10-31assouplissement de la syntaxe du let de ltac: t1 ; let in autorisebarras
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
2006-10-24Extension de la primitive ltac fresh pour qu'elle accepte une liste deherbelin
2006-07-11Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...herbelin
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-01-21Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...herbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-07-16Suppression quotifyherbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...herbelin
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte des...herbelin
2004-01-02meilleure presentation des commentaires du traducteurbarras
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-10-16nouvelle syntaxe de ltacbarras
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-05-24Ajout FreshIdherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-14reparations suite a la nouvelle syntaxe:barras
2003-03-12*** empty log message ***barras
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin