diff options
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 |