diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 11 | ||||
| -rw-r--r-- | interp/genarg.mli | 10 |
2 files changed, 12 insertions, 9 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 2e057e438b..d98788eede 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -16,6 +16,7 @@ open Nametab open Rawterm open Topconstr open Term +open Evd type argument_type = (* Basic types *) @@ -47,6 +48,10 @@ type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = AN of 'a | ByNotation of loc * string type rawconstr_and_expr = rawconstr * constr_expr option +type open_constr_expr = unit * constr_expr +type open_rawconstr = unit * rawconstr_and_expr + +type 'a with_ebindings = 'a * open_constr bindings (* Dynamics but tagged by a type expression *) @@ -56,7 +61,7 @@ let dyntab = ref ([] : string list) type rlevel = constr_expr type glevel = rawconstr_and_expr -type tlevel = constr +type tlevel = open_constr type ('a,'b) abstract_argument_type = argument_type @@ -90,10 +95,6 @@ and pr_case_intro_pattern = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" -type open_constr = Evd.evar_map * Term.constr -type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr - let rawwit_bool = BoolArgType let globwit_bool = BoolArgType let wit_bool = BoolArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index db078bfc1e..ccaf93d58c 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -15,6 +15,7 @@ open Libnames open Rawterm open Topconstr open Term +open Evd type 'a and_short_name = 'a * identifier located option @@ -25,10 +26,11 @@ type 'a or_by_notation = AN of 'a | ByNotation of loc * string (* The [constr_expr] field is [None] in TacDef though *) type rawconstr_and_expr = rawconstr * constr_expr option -type open_constr = Evd.evar_map * Term.constr type open_constr_expr = unit * constr_expr type open_rawconstr = unit * rawconstr_and_expr +type 'a with_ebindings = 'a * open_constr bindings + type intro_pattern_expr = | IntroOrAndPattern of case_intro_pattern_expr | IntroWildcard @@ -106,7 +108,7 @@ ExtraArgType of string '_a '_b type rlevel = constr_expr type glevel = rawconstr_and_expr -type tlevel = constr +type tlevel = open_constr type ('a,'co) abstract_argument_type @@ -176,11 +178,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_bindings,tlevel) abstract_argument_type +val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (constr bindings,tlevel) abstract_argument_type +val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type |