diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/include | 3 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 |
3 files changed, 4 insertions, 1 deletions
@@ -33,6 +33,7 @@ install_printer Top_printers.pptype install_printer Top_printers.ppj install_printer Top_printers.ppenv install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm diff --git a/dev/include b/dev/include index 7c63f54436..941fa3383b 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;;*) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fccf580a50..15f35b775f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -141,6 +141,7 @@ let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) +let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) |