From 0276f8357a2ea1d83cb6b85b86b8b3f5a1e4579d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 28 Dec 2014 11:43:01 +0100
Subject: remove debug prints (leftover)

---
 proofs/proof_using.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'proofs/proof_using.ml')

diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 144646f3e8..d4e97a23ff 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -60,11 +60,7 @@ and full_set env = set_of_list env (List.map pi1 (named_context env))
 
 let process_expr env e ty =
   let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
-  let l = Id.Set.elements s in
-  Pp.msg_warning Pp.(str(to_string e) ++ spc() ++ str "-> "++
-(*     prlist_with_sep spc Ppconstr.pr_constr ty ++ spc() ++ *)
-    prlist_with_sep spc Nameops.pr_id l);
-  l
+  Id.Set.elements s
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
 
-- 
cgit v1.2.3