From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 17:02:04 +0000 (+0000)
Subject: Use seed to avoid further name clashes.
X-Git-Tag: make_still_working~5399
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ac31c84bb9bcf327554976d4296d787853fc8db5;p=helm.git

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 767634329..a9c8d11ef 100644
--- 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