Fixes on functional graphs merging: removed debug printing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9296 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 10 deletions

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 1a960b0ee..ba97ff4eb 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -560,18 +560,19 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
   typwithprms
 
 
+(** Return true id [id] is linked in global environment *)
+let ident_global_exist id = 
+  try 
+    let ans = CRef (Libnames.Ident (dummy_loc,id)) in
+    let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
+    true
+  with _ -> false 
+    
 let next_ident_fresh (s:identifier) = 
     let res = ref s in
-    let _ = prstr (Printf.sprintf "\ns = %s" (string_of_id !res)) in
-    while 
-      (try
-          let ans = CRef (Libnames.Ident (dummy_loc,!res)) in
-          ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans)
- (* ignore (Prettyp.locate_any_name Libnames.qualid_of_string (string_of_id !res)) *)
-      ; true 
-      with _ -> false)
-    do res := Nameops.lift_ident !res ; prstr (string_of_id !res) done;
-    let _ = prstr (Printf.sprintf "\ns = %s (out)" (string_of_id !res)) in
+    while ident_global_exist !res do
+      res := Nameops.lift_ident !res ; prstr (string_of_id !res) 
+    done;
     !res;;
 
 (*