aboutsummaryrefslogtreecommitdiff
path: root/parsing/argextend.ml4
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2006-10-24Hack peu élégant pour permettre de parser des listes avec séparateurs dans herbelin
2006-06-23Suppresion redondance interp_entry_name entre Q_util et Argextendherbelin
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
2005-12-26Petite correction nom QuantHypArgType suite suppression traducteurherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-18*** empty log message ***barras
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification n...herbelin
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-07-20Abstraction vis à vis de dummy_locherbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-17Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsherbelin
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...herbelin
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte des...herbelin
2003-12-01Nouvelle tactique EExistsclrenard
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
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-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin