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

6 files changed, 40 insertions, 9 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index ea8302e91c..9975f38487 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Names
 open Glob_term
 open Constrexpr
 open Misctypes
@@ -238,3 +239,17 @@ let default_empty_value t =
   match aux t with
   | Some v -> Some (out_gen t v)
   | None -> None
+
+(** New interface for genargs. *)
+
+type glob_sign = {
+  ltacvars : Id.t list * Id.t list;
+  ltacrecvars : (Id.t * Nametab.ltac_constant) list;
+  gsigma : Evd.evar_map;
+  genv : Environ.env }
+
+module TacStore = Store.Make(struct end)
+
+type interp_sign = {
+  lfun : (Id.t * tlevel generic_argument) list;
+  extra : TacStore.t }
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 8f4b816187..ff70bd7a24 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -17,7 +17,6 @@ open Genredexpr
 open Pattern
 open Constrexpr
 open Term
-open Evd
 open Misctypes
 
 (** FIXME: nothing to do there. *)
@@ -200,6 +199,20 @@ val app_pair :
       ('a generic_argument -> 'b generic_argument)
    -> 'a generic_argument -> 'b generic_argument
 
+(** {6 High-level creation} *)
+
+type glob_sign = {
+  ltacvars : Id.t list * Id.t list;
+  ltacrecvars : (Id.t * Nametab.ltac_constant) list;
+  gsigma : Evd.evar_map;
+  genv : Environ.env }
+
+module TacStore : Store.S
+
+type interp_sign = {
+  lfun : (Id.t * tlevel generic_argument) list;
+  extra : TacStore.t }
+
 (** {6 Type reification} *)
 
 type argument_type =
@@ -239,6 +252,8 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
 (** {6 Ground types} *)
 
+open Evd
+
 val wit_bool : bool uniform_genarg_type
 
 val wit_int : int uniform_genarg_type
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 883b9094f2..dc84fa5922 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 c928b73799..75576516f4 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 76c7dfeb35..e52c2fe248 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 1be34a90f3..f079d1dfbd 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 }