Name capture fixed.

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index e414cfa56dc4061d32c2485ed1a1105d709b91ac..b1b08ee3c7821db86fd7186e588c04467f7cf62f 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -194,6 +194,14 @@ let fix_outtype t =
   aux [] t
 ;;
 
+let get_fresh,reset_seed =
+ let seed = ref 0 in
+  (function () ->
+   incr seed;
+   string_of_int !seed),
+  (function () -> seed := 0)
+;;
+
 (* 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,7 +211,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 
@@ -241,7 +249,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 
@@ -375,8 +383,8 @@ let convert_term uri t =
       in
       let ens,objs =
        List.fold_right
-        (fun uri (l,objs) ->
-          let t = List.assoc uri ens in
+        (fun luri (l,objs) ->
+          let t = List.assoc luri ens in
           let t,o = aux octx ctx n_fix uri t in
            t::l, o@objs
         ) params ([],[])
@@ -454,6 +462,7 @@ let convert_obj_aux uri = function
 ;;
 
 let convert_obj uri obj = 
+  reset_seed ();
   let o, fixpoints = convert_obj_aux uri obj in
   let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in
   fixpoints @ [obj]