aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_ltacnew.ml4
AgeCommit message (Expand)Author
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-06-22Added entry constr_may_eval for tactic extensions (new syntax)herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-09possibilité d'écrire [foo| ] au lieu de [foo|idtac]letouzey
2005-02-04Ajout constructeur External pour appel outil externe à Coqherbelin
2004-10-12Desactivation de la construction 'lazy match' en attendant une autre solutionherbelin
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
2003-12-23*** empty log message ***barras
2003-12-04Symetrisation parsing/printing 'abstract'herbelin
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-12petits changements de syntaxebarras
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-09-21Parsing au niveau lconstr des patterns de 'match context'herbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10freshid -> freshherbelin
2003-05-26Bugherbelin
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-27MAJ des mots-clés, Definition, Theorem, ...herbelin
2003-03-12*** empty log message ***barras