From 10a347a382773cf6567669005730bb5ed8775416 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Jun 2013 16:11:22 +0000
Subject: 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
---
 interp/genarg.ml  | 15 +++++++++++++++
 interp/genarg.mli | 17 ++++++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)

(limited to 'interp')

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
-- 
cgit v1.2.3