aboutsummaryrefslogtreecommitdiff
path: root/parsing/tactic_printer.ml
AgeCommit message (Expand)Author
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras