Merge PR#608: Allow Ltac2 as a plugin

1 files changed, 7 insertions, 3 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3b3dccc998..c7078cf2a0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -69,6 +69,7 @@ type internalization_env =
 type ltac_sign = {
   ltac_vars : Id.Set.t;
   ltac_bound : Id.Set.t;
+  ltac_extra : Genintern.Store.t;
 }
 
 let interning_grammar = ref false
@@ -1733,12 +1734,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         | Some gen ->
           let (ltacvars, ntnvars) = lvar in
           let ntnvars = Id.Map.domain ntnvars in
+          let extra = ltacvars.ltac_extra in
           let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
           let lvars = Id.Set.union lvars ntnvars in
-          let lvars = Id.Set.union lvars env.ids in
+          let ltacvars = Id.Set.union lvars env.ids in
           let ist = {
-            Genintern.ltacvars = lvars;
-            genv = globalenv;
+            Genintern.genv = globalenv;
+            ltacvars;
+            extra;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
@@ -1937,6 +1940,7 @@ let scope_of_type_kind = function
 let empty_ltac_sign = {
   ltac_vars = Id.Set.empty;
   ltac_bound = Id.Set.empty;
+  ltac_extra = Genintern.Store.empty;
 }
 
 let intern_gen kind env