aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-09-27 14:11:36 +0200
committerPierre-Marie Pédrot2018-09-27 14:11:36 +0200
commit64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (patch)
tree3171d8632e1dd95072c93b76a9627d4c0363ae96 /pretyping/reductionops.mli
parent523c5e41f78dbd4dfbb60d4d7c78f01a22b30aa2 (diff)
parent7628af7af9ff20d2a894673f66c3753e214623f1 (diff)
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index dd3cd26f0f..c0ff6723f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -60,7 +60,7 @@ module Cst_stack : sig
val best_cst : t -> (constr * constr list) option
val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
val reference : Evd.evar_map -> t -> Constant.t option
- val pr : t -> Pp.t
+ val pr : env -> Evd.evar_map -> t -> Pp.t
end
module Stack : sig
@@ -140,7 +140,7 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-val pr_state : state -> Pp.t
+val pr_state : env -> evar_map -> state -> Pp.t
(** {6 Reduction Function Operators } *)