diff options
| author | Maxime Dénès | 2020-06-05 11:29:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-05 11:29:05 +0200 |
| commit | 0379ab63a3a84bae6da8b8d5ae42af4261520279 (patch) | |
| tree | 4f723436356a436274c75d16741da528ae07237e /dev | |
| parent | 0ae20176df146b90f11e131aff3673584e6ffb3a (diff) | |
| parent | 497a300a7f50d2f4a37dae5c3d6fdab870829051 (diff) | |
Merge PR #11707: Split the Reductionops machine from the cbn one
Reviewed-by: maximedenes
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/include_printers | 1 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | dev/top_printers.mli | 1 |
4 files changed, 0 insertions, 4 deletions
diff --git a/dev/include_printers b/dev/include_printers index d077075eeb..30529b5fd6 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -27,7 +27,6 @@ #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;; (*#install_printer (* hint_db *) print_hint_db;;*) diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 06db787488..63071bba72 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -46,7 +46,6 @@ install_printer Top_printers.pp_idpred install_printer Top_printers.pp_cpred install_printer Top_printers.pp_transparent_state install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t install_printer Top_printers.pp_state_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm 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 *) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index c826391cac..65eab8daa3 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -106,7 +106,6 @@ val pp_cpred : Names.Cpred.t -> unit val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit -val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit val pp_state_t : Reductionops.state -> unit val ppmetas : Evd.Metaset.t -> unit |