diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-30 16:51:34 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-30 16:51:34 +0000 |
| commit | 4d58a4f25a796d1c5d39f2be8648696cdfd46dba (patch) | |
| tree | 3b2587eb464393caf23a50283c10f80532ace22f /plugins/cc/ccalgo.ml | |
| parent | 24879dc0e59856e297b0172d00d67df67fbb0184 (diff) | |
Getting rid of Pp.msg
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 7434f5e8a..699f1f3df 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 |