diff options
| author | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
| commit | 6a48e732577b9ab09d458c7526f599d4528fe2fc (patch) | |
| tree | 66cf1df2a49a7ee2470d13dd46b3ee917cdc00e3 /engine | |
| parent | 5ced288419aed8a622ed2c267e35d9a174facafc (diff) | |
| parent | 39a10cba3d610c6f12438084c5de7c1217c8fe94 (diff) | |
Merge PR #8534: Checking if low-level name printers are used on purpose or not
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | engine/termops.mli | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 156d1370e3..710743e92d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -49,6 +49,8 @@ let pr_puniverses p u = if Univ.Instance.is_empty u then p else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" +(* Minimalistic constr printer, typically for debugging *) + let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" diff --git a/engine/termops.mli b/engine/termops.mli index b967bb6abb..9ce2db9234 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,11 +311,17 @@ 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 -(** debug printer: do not use to display terms to the casual user... *) +(** Internal hook to register user-level printer *) val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit + +(** User-level printers *) + val print_constr : constr -> Pp.t val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t + +(** debug printer: do not use to display terms to the casual user... *) + val print_named_context : env -> Pp.t val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t |