aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/argextend.ml4
Commit message (Expand)AuthorAge
* 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