Merge PR #12708: Do not store the full environment inside ssr ast_closure_term.

Reviewed-by: gares

4 files changed, 26 insertions, 2 deletions

diff --git a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst
new file mode 100644
index 0000000000..4df8e97e34
--- /dev/null
+++ b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Do not store the full environment inside ssr ast_closure_term
+  (`#12708 <https://github.com/coq/coq/pull/12708>`_,
+  fixes `#12707 <https://github.com/coq/coq/issues/12707>`_,
+  by Pierre-Marie Pédrot).
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 8adffdc709..f6a741f468 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -51,13 +51,19 @@ type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
 
 (* NEW ssr term *)
 
+type ast_glob_env = {
+  ast_ltacvars : Id.Set.t;
+  ast_extra : Genintern.Store.t;
+  ast_intern_sign : Genintern.intern_variable_status;
+}
+
 (* These terms are raw but closed with the intenalization/interpretation
  * context.  It is up to the tactic receiving it to decide if such contexts
  * are useful or not, and eventually manipulate the term before turning it
  * into a constr *)
 type ast_closure_term = {
   body : Constrexpr.constr_expr;
-  glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *)
+  glob_env : ast_glob_env option; (* for Tacintern.intern_constr *)
   interp_env :  Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *)
   annotation : [ `None | `Parens | `DoubleParens | `At ];
 }
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 65204b7868..ba978c0705 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -302,6 +302,11 @@ let mk_ast_closure_term a t = {
 }
 
 let glob_ast_closure_term (ist : Genintern.glob_sign) t =
+  let ist = {
+    ast_ltacvars = ist.Genintern.ltacvars;
+    ast_intern_sign = ist.Genintern.intern_sign;
+    ast_extra = ist.Genintern.extra;
+  } in
   { t with glob_env = Some ist }
 let subst_ast_closure_term (_s : Mod_subst.substitution) t =
   (* _s makes sense only for glob constr *)
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index ad0a31622c..d99ead139d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -150,7 +150,15 @@ let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } =
     let sigma = sigma goal in
     let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
     (* We use the env of the goal, not the global one *)
-    let ist = { ist with Genintern.genv } in
+    let ist =
+      let open Genintern in
+      {
+        ltacvars = ist.ast_ltacvars;
+        extra = ist.ast_extra;
+        intern_sign = ist.ast_intern_sign;
+        genv;
+      }
+    in
     (* We open extra_scope *)
     let body =
       match extra_scope with