X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=extracted%2Fglobalenvs.ml;fp=extracted%2Fglobalenvs.ml;h=3e52b9c169832287b833151cdb6d082d36265bbb;hb=d549e01e37d9b10e96f60e64a1814f5a9208e283;hp=1ae2aa34e01ffcf9d2d3782bfd976fb6299f310a;hpb=b4da02b8856ccc723c707618038f6a5c3bf223e2;p=pkg-cerco%2Facc-trusted.git

diff --git a/extracted/globalenvs.ml b/extracted/globalenvs.ml
index 1ae2aa3..3e52b9c 100644
--- a/extracted/globalenvs.ml
+++ b/extracted/globalenvs.ml
@@ -313,8 +313,8 @@ let size_init_data_list i_data =
     genv_t, GenMem.mem) Types.prod **)
 let add_globals extract_init init_env vars =
   Util.foldl (fun g_st id_init ->
-    let { Types.fst = eta1345; Types.snd = init_info } = id_init in
-    let { Types.fst = id; Types.snd = r } = eta1345 in
+    let { Types.fst = eta1367; Types.snd = init_info } = id_init in
+    let { Types.fst = id; Types.snd = r } = eta1367 in
     let init = extract_init init_info in
     let { Types.fst = g; Types.snd = st } = g_st in
     let { Types.fst = st'; Types.snd = b } =
@@ -329,8 +329,8 @@ let add_globals extract_init init_env vars =
     GenMem.mem Errors.res **)
 let init_globals extract_init g m vars =
   Util.foldl (fun st id_init ->
-    let { Types.fst = eta1346; Types.snd = init_info } = id_init in
-    let { Types.fst = id; Types.snd = r } = eta1346 in
+    let { Types.fst = eta1368; Types.snd = init_info } = id_init in
+    let { Types.fst = id; Types.snd = r } = eta1368 in
     let init = extract_init init_info in
     Obj.magic
       (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->