X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=6987bb7ebfe663003268f72bdb525217ad38042e;hb=52a90cb35796f2f090c97e41dc13ab1715877234;hp=a9c8d11efc42c26f5d4f821878950b00cea4a23f;hpb=ac31c84bb9bcf327554976d4296d787853fc8db5;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index a9c8d11ef..6987bb7eb 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -194,11 +194,12 @@ let fix_outtype t =
   aux [] t
 ;;
 
-let get_fresh =
+let get_fresh,reset_seed =
  let seed = ref 0 in
-  function () ->
+  (function () ->
    incr seed;
-   string_of_int !seed
+   string_of_int !seed),
+  (function () -> seed := 0)
 ;;
 
 (* we are lambda-lifting also variables that do not occur *)
@@ -461,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]