aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_ltac.ml4
Commit message (Expand)AuthorAge
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Correction de bugs:Gravatar herbelin2008-08-05
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Diverses corrections Gravatar herbelin2008-04-14
* suppression code mort oublié lors du commit 10495Gravatar herbelin2008-02-10
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsGravatar herbelin2007-02-15
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* syntaxe du let in encoreGravatar barras2006-10-31
* assouplissement de la syntaxe du let de ltac: t1 ; let in autoriseGravatar barras2006-10-31
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
* Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...Gravatar herbelin2006-07-11
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...Gravatar herbelin2006-03-05
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...Gravatar herbelin2006-01-21
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* Suppression quotifyGravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...Gravatar herbelin2004-03-02
* Généralisation du type ltac Identifier en IntroPattern; prise en compte des...Gravatar herbelin2004-03-01
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...Gravatar herbelin2003-09-12
* Ajout FreshIdGravatar herbelin2003-05-24
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* reparations suite a la nouvelle syntaxe:Gravatar barras2003-03-14
* *** empty log message ***Gravatar barras2003-03-12
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19