After generalization of theories, remember work obtained by the theory

src/ecSection.ml

@@ -1470,20 +1470,20 @@ and generalize_ctheory
     add_clear genenv (`Th path)
   else
     let scenv = enter_theory name `Global cth.cth_mode genenv.tg_env in
-    let genenv_tmp = List.fold_left
+    let genenv_thy = List.fold_left
       (fun x -> generalize_th_item x path)
       { genenv with tg_env = scenv } cth.cth_items in
 
-    let _, compiled, _ = exit_theory genenv_tmp.tg_env in
+    let _, compiled, _ = exit_theory genenv_thy.tg_env in
 
     match compiled with
     | None ->
-      genenv
+      { genenv_thy with tg_env = genenv.tg_env }
     | Some compiled when List.is_empty compiled.ctheory.cth_items ->
-      genenv
+      { genenv_thy with tg_env = genenv.tg_env }
     | Some compiled ->
       let scenv = add_th ~import:true compiled genenv.tg_env in
-      { genenv with tg_env = scenv; }
+      { genenv_thy with tg_env = scenv; }
 
 and generalize_lc_item (genenv : to_gen) (prefix : path) (item : sc_item) =
   match item with

tests/theory-in-section-w-declare-type.ec

@@ -0,0 +1,16 @@
+section.
+    declare type t.
+
+    theory T.
+        op foo : t.
+    end T.
+
+    op bar : t = T.foo.
+end section.
+
+lemma L (y x : unit): (idfun bar = y) =>
+idfun T.foo = x /\ idfun bar = y.
+proof.
+move => yP.
+rewrite yP.
+abort.