Merge PR#608: Allow Ltac2 as a plugin

4 files changed, 27 insertions, 5 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
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fdd50c6a1e..644cafe575 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -70,6 +70,8 @@ type ltac_sign = {
   (** Variables of Ltac which may be bound to a term *)
   ltac_bound : Id.Set.t;
   (** Other variables of Ltac *)
+  ltac_extra : Genintern.Store.t;
+  (** Arbitrary payload *)
 }
 
 val empty_ltac_sign : ltac_sign
diff --git a/interp/genintern.ml b/interp/genintern.ml
index be7abfa995..e443824bd2 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,9 +10,19 @@ open Names
 open Mod_subst
 open Genarg
 
+module Store = Store.Make(struct end)
+
 type glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Store.t;
+}
+
+let empty_glob_sign env = {
+  ltacvars = Id.Set.empty;
+  genv = env;
+  extra = Store.empty;
+}
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4b0354be39..658caa08c2 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -10,9 +10,15 @@ open Names
 open Mod_subst
 open Genarg
 
+module Store : Store.S
+
 type glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Store.t;
+}
+
+val empty_glob_sign : Environ.env -> glob_sign
 
 (** {5 Internalization functions} *)