4 files changed, 22 insertions, 5 deletions
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..1b7768852e 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 *)
@@ -1124,8 +1129,7 @@ let tclDO n tac =
       let _, info = Exninfo.capture e in
       let e' = CErrors.UserError (l, prefix i ++ s) in
       Exninfo.iraise (e', info)
-    | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
-      raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+  in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a12b4aad11..1c81fbc10b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -490,7 +490,6 @@ let equality_inj l b id c =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
-    | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||
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