From 2f0762ba5463efba7c5ca7c5e39b947b8cad1fd3 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Thu, 18 Jun 2026 19:05:06 +0200
Subject: [PATCH] During generalization of theories, remember work obtained by
 the theory

---
 src/ecSection.ml                          |  6 +++---
 tests/theory-in-section-w-declare-type.ec | 12 ++++++++++++
 2 files changed, 15 insertions(+), 3 deletions(-)
 create mode 100644 tests/theory-in-section-w-declare-type.ec

diff --git a/src/ecSection.ml b/src/ecSection.ml
index bf98fdd8c..ca838b20b 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -1478,12 +1478,12 @@ and generalize_ctheory
 
     match compiled with
     | None ->
-      genenv
+      { genenv_tmp with tg_env = genenv.tg_env }
     | Some compiled when List.is_empty compiled.ctheory.cth_items ->
-      genenv
+      { genenv_tmp 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_tmp with tg_env = scenv; }
 
 and generalize_lc_item (genenv : to_gen) (prefix : path) (item : sc_item) =
   match item with
diff --git a/tests/theory-in-section-w-declare-type.ec b/tests/theory-in-section-w-declare-type.ec
new file mode 100644
index 000000000..c814936ba
--- /dev/null
+++ b/tests/theory-in-section-w-declare-type.ec
@@ -0,0 +1,12 @@
+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.
+move => yP.
+rewrite yP.