From bcfd854d7a6e012ac6bf116487a59a0f997725ee Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 30 Jun 2014 18:05:39 +0200 Subject: Debug RAKAM --- dev/include | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dev/include') diff --git a/dev/include b/dev/include index 7c63f5443..941fa3383 100644 --- a/dev/include +++ b/dev/include @@ -53,7 +53,8 @@ #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; -#install_printer (* judgement *) pp_cst_stack_t;; +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; (*#install_printer (* hint_db *) print_hint_db;;*) (*#install_printer (* hints_path *) pphintspath;;*) -- cgit v1.2.3