From ac31c84bb9bcf327554976d4296d787853fc8db5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 17:02:04 +0000 Subject: [PATCH] Use seed to avoid further name clashes. --- helm/software/components/ng_kernel/oCic2NCic.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) 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 -- 2.39.2