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 /plugins/cc | |
| parent | 523c5e41f78dbd4dfbb60d4d7c78f01a22b30aa2 (diff) | |
| parent | 7628af7af9ff20d2a894673f66c3753e214623f1 (diff) | |
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index ce620d5312..f26ec0f401 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -26,6 +26,10 @@ let init_size=5 let cc_verbose=ref false +let print_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t + let debug x = if !cc_verbose then Feedback.msg_debug (x ()) @@ -483,10 +487,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end |