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 /engine/termops.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 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 32 |
1 files changed, 27 insertions, 5 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 9ce2db9234..aa0f837938 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,18 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t -(** Internal hook to register user-level printer *) +module Internal : sig -val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit +(** NOTE: to print terms you always want to use functions in + Printer, not these ones which are for very special cases. *) -(** User-level printers *) +(** debug printers: print raw form for terms, both with + evar-substitution and without. *) +val debug_print_constr : constr -> Pp.t +val debug_print_constr_env : env -> evar_map -> constr -> Pp.t -val print_constr : constr -> Pp.t +(** Pretty-printer hook: [print_constr_env env sigma c] will pretty + print c if the pretty printing layer has been linked into the Coq + binary. *) val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t -(** debug printer: do not use to display terms to the casual user... *) +(** [set_print_constr f] sets f to be the pretty printer *) +val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit +(** Printers for contexts *) val print_named_context : env -> Pp.t val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t + +val print_constr : constr -> Pp.t +[@@deprecated "use print_constr_env"] + +end + +val print_constr : constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_rel_context : env -> Pp.t +[@@deprecated "use Internal.print_rel_context"] |