aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pptactic.mli
Commit message (Expand)AuthorAge
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Correction printer des Tactic NotationGravatar herbelin2005-12-23
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* Simplification afficheur de tactiques non primitiveGravatar herbelin2003-09-18
* Traduction des réferences arguments de commandes non primitivesGravatar herbelin2003-09-09
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Debugger plus informatifGravatar delahaye2003-02-13
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29