From 4d58a4f25a796d1c5d39f2be8648696cdfd46dba Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 30 May 2012 16:51:34 +0000
Subject: Getting rid of Pp.msg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/ccalgo.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/cc/ccalgo.ml')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 7434f5e8a5..699f1f3dfd 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -696,14 +696,15 @@ type explanation =
 let check_disequalities state =
   let uf=state.uf in
   let rec check_aux = function
-      dis::q ->
-	debug (fun () -> msg
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();
-	if find uf dis.lhs=find uf dis.rhs then
-	  begin debug msgnl (str "Yes");Some dis end
-	else
-	  begin debug msgnl (str "No");check_aux q end
+    | dis::q ->
+        let (info, ans) =
+          if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
+          else (str "No", check_aux q)
+        in
+        let _ = debug (fun () -> msg_debug
+        (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+         pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+        ans
     | [] -> None
   in
     check_aux state.diseq
-- 
cgit v1.2.3