aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-02-11 22:07:31 +0100
committerPierre-Marie Pédrot2020-06-04 12:44:45 +0200
commit7a8c4003ef5071d6b9bc248e997d0397304e8491 (patch)
treea2994e5cd0a245aa756125ceb8626bbc093f45a8 /dev/top_printers.ml
parente766d31683550d1debea70a3620fc3597a154700 (diff)
Move the cbn reduction to its own file, and simplify the RAKAM accordingly.
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 00050a89e1..bca1eb5754 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -169,7 +169,6 @@ let pp_idpred s = pp (pr_idpred s)
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 (EConstr.of_constr %> pr_econstr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
(* proof printers *)