Use seed to avoid further name clashes.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 767634329b0ff8971559b79f060758129aa3fad3..a9c8d11efc42c26f5d4f821878950b00cea4a23f 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -194,6 +194,13 @@ let fix_outtype t =
   aux [] t
 ;;
 
+let get_fresh =
+ let seed = ref 0 in
+  function () ->
+   incr seed;
+   string_of_int !seed
+;;
+
 (* we are lambda-lifting also variables that do not occur *)
 (* ctx does not distinguish successive blocks of cofix, since there may be no
  *   lambda separating them *)
@@ -203,8 +210,7 @@ let convert_term uri t =
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
-            UriManager.name_of_uri uri ^ "___" ^
-             string_of_int (List.length ctx)^".con")
+            UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con")
         in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
@@ -242,8 +248,7 @@ let convert_term uri t =
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
-            UriManager.name_of_uri uri ^ "___" ^
-             string_of_int (List.length ctx)^".con")
+            UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con")
         in
         let bad_bctx, fixpoints_tys, tys, _ = 
           List.fold_right