diff options
| author | Pierre-Marie Pédrot | 2018-09-27 14:11:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-27 14:11:36 +0200 |
| commit | 64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (patch) | |
| tree | 3171d8632e1dd95072c93b76a9627d4c0363ae96 /proofs | |
| parent | 523c5e41f78dbd4dfbb60d4d7c78f01a22b30aa2 (diff) | |
| parent | 7628af7af9ff20d2a894673f66c3753e214623f1 (diff) | |
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 79b7e1599b..95e908c4dd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -575,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma let pr_clenv clenv = h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ + (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ + str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 092bb5c276..182b38d350 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -127,8 +127,8 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in - let penv = print_named_context env in - let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in + let penv = Termops.Internal.print_named_context env in + let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () |