diff options
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/dev/include b/dev/include index eabf79a481..d1b5a717b4 100644 --- a/dev/include +++ b/dev/include @@ -4,10 +4,6 @@ #cd ".";; #use "base_include";; -#install_printer (* ast *) prast;; -#install_printer (* pat *) prastpat;; -#install_printer (* patlist *) prastpatl;; - #install_printer (* pattern *) pppattern;; #install_printer (* rawconstr *) pprawterm;; |