aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/argextend.ml4
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Hack peu élégant pour permettre de parser des listes avec séparateurs dans Gravatar herbelin2006-10-24
* Suppresion redondance interp_entry_name entre Q_util et ArgextendGravatar herbelin2006-06-23
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Petite correction nom QuantHypArgType suite suppression traducteurGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* *** empty log message ***Gravatar barras2005-11-18
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Abstraction vis à vis de dummy_locGravatar herbelin2004-07-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsGravatar herbelin2004-06-17
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Généralisation du type ltac Identifier en IntroPattern; prise en compte des...Gravatar herbelin2004-03-01
* Nouvelle tactique EExistsGravatar clrenard2003-12-01
* New tactics : econstructor, eleft, eright, esplitGravatar clrenard2003-11-17
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...Gravatar herbelin2002-06-05