diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/include | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 7f72f55d9d..b2eb280d6c 100644 --- a/dev/include +++ b/dev/include @@ -52,6 +52,8 @@ #install_printer (* 'a scheme_kind *) ppscheme;; #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; +#install_printer (* id set *) ppidset;; +#install_printer (* int set *) ppintset;; #install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; #install_printer (* Reductionops machine stack *) pp_stack_t;; |