Now glob_sign and interp_sign only depend on structures defined

upto Genarg, so moved them there. This will allow defining the new
genarg interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 9 insertions, 8 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 883b9094f..dc84fa592 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -52,7 +52,7 @@ let skip_metaid = function
 
 (** Generic arguments *)
 
-type glob_sign = {
+type glob_sign = Genarg.glob_sign = {
   ltacvars : Id.t list * Id.t list;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   ltacrecvars : (Id.t * ltac_constant) list;
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index c928b7379..75576516f 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -23,7 +23,7 @@ open Nametab
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
-type glob_sign = {
+type glob_sign = Genarg.glob_sign = {
   ltacvars : Id.t list * Id.t list;
   ltacrecvars : (Id.t * ltac_constant) list;
   gsigma : Evd.evar_map;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 76c7dfeb3..e52c2fe24 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -36,9 +36,6 @@ open Genarg
 open Printer
 open Pretyping
 open Extrawit
-
-module TacStore = Store.Make(struct end)
-
 open Evd
 open Misctypes
 open Miscops
@@ -88,13 +85,15 @@ let catch_error call_trace tac g =
     raise located_exc
   end
 
+module TacStore = Genarg.TacStore
+
 let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
 (* ids inherited from the call context (needed to get fresh ids) *)
 let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = {
+type interp_sign = Genarg.interp_sign = {
   lfun : (Id.t * value) list;
   extra : TacStore.t }
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 1be34a90f..f079d1dfb 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -32,10 +32,12 @@ end
 (** Values for interpretation *)
 type value = Value.t
 
-module TacStore : Store.S
+module TacStore : Store.S with
+  type t = Genarg.TacStore.t
+  and type 'a field = 'a Genarg.TacStore.field
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
-type interp_sign = {
+type interp_sign = Genarg.interp_sign = {
   lfun : (Id.t * value) list;
   extra : TacStore.t }