diff options
| author | Emilio Jesus Gallego Arias | 2017-12-29 20:20:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-26 16:33:48 +0200 |
| commit | 7628af7af9ff20d2a894673f66c3753e214623f1 (patch) | |
| tree | bb4c10fea3e44e6949a00d591234cecfc3f345ee /pretyping/reductionops.mli | |
| parent | f49928874b51458fb67e89618bb350ae2f3529e4 (diff) | |
[print] Restrict use of "debug" Termops printer.
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
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 } *) |