diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 11:20:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 12:22:45 +0100 |
| commit | 4e6d36c5977a874dc5adcdfb041c0a40c340e0b7 (patch) | |
| tree | 5324904279dea705b024d774e2c90a991291833d /dev/include | |
| parent | 603b66f81ba876d97b5d245154c692df2e409fa5 (diff) | |
More printers in tracer.
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 7f72f55d9..b2eb280d6 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;; |