| Commit message (Expand) | Author | Age |
* | ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED | glondu | 2010-12-25 |
* | Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands | glondu | 2010-12-25 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Finish adding out-of-the-box support for camlp4 | letouzey | 2010-07-09 |
* | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
* | Nicer representation of tokens, more independant of camlp* | letouzey | 2010-05-19 |
* | static (and shared) camlp4use instead of per-file declaration | letouzey | 2010-05-19 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | - 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 | 2009-04-27 |
* | Fixed bug in VernacExtend printing + missing vernacular printing rules + | herbelin | 2008-11-22 |
* | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
* | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey | 2007-09-15 |
* | Generalized CAMLP4USE for pp dependencies | corbinea | 2007-07-16 |
* | Hack peu élégant pour permettre de parser des listes avec séparateurs dans | herbelin | 2006-10-24 |
* | Suppresion redondance interp_entry_name entre Q_util et Argextend | herbelin | 2006-06-23 |
* | Changement du type d'argument 'TacticArgType X' en un type | herbelin | 2006-06-08 |
* | Petite correction nom QuantHypArgType suite suppression traducteur | herbelin | 2005-12-26 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | *** empty log message *** | barras | 2005-11-18 |
* | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
* | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin | 2005-05-17 |
* | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin | 2004-12-09 |
* | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin | 2004-12-06 |
* | Abstraction vis à vis de dummy_loc | herbelin | 2004-07-20 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | moved instantiate binding to extratactics | corbinea | 2004-06-29 |
* | Nouvelle syntaxe à la ML pour donner le type ML des extensions d'arguments | herbelin | 2004-06-17 |
* | Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no... | herbelin | 2004-03-02 |
* | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin | 2004-03-01 |
* | Nouvelle tactique EExists | clrenard | 2003-12-01 |
* | New tactics : econstructor, eleft, eright, esplit | clrenard | 2003-11-17 |
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
* | *** empty log message *** | barras | 2003-03-12 |
* | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin | 2003-01-19 |
* | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
* | Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar... | herbelin | 2002-06-05 |