From 7628af7af9ff20d2a894673f66c3753e214623f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 29 Dec 2017 20:20:38 +0100
Subject: [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.
---
 plugins/cc/ccalgo.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'plugins/cc')

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
-- 
cgit v1.2.3