diff options
| author | ppedrot | 2013-06-18 16:11:22 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-18 16:11:22 +0000 |
| commit | 10a347a382773cf6567669005730bb5ed8775416 (patch) | |
| tree | e432395739f888f1ae4698216ec673e76ee2073e /interp | |
| parent | 9af59cbf531b31b144e5aeaa2d62b0669bd37de0 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 15 | ||||
| -rw-r--r-- | interp/genarg.mli | 17 |
2 files changed, 31 insertions, 1 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 |