aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml4
-rw-r--r--grammar/argextend.ml495
-rw-r--r--grammar/tacextend.ml47
-rw-r--r--interp/genarg.ml55
-rw-r--r--interp/genarg.mli176
-rw-r--r--parsing/extrawit.ml30
-rw-r--r--parsing/extrawit.mli35
-rw-r--r--parsing/g_obligations.ml49
-rw-r--r--parsing/pcoq.ml446
-rw-r--r--plugins/decl_mode/g_decl_mode.ml416
-rw-r--r--plugins/funind/g_indfun.ml46
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--printing/ppextra.ml8
-rw-r--r--printing/pptactic.ml112
-rw-r--r--printing/pptactic.mli8
-rw-r--r--tactics/eauto.mli10
-rw-r--r--tactics/extraargs.ml48
-rw-r--r--tactics/extraargs.mli35
-rw-r--r--tactics/rewrite.ml49
-rw-r--r--tactics/tacintern.ml54
-rw-r--r--tactics/tacinterp.ml122
-rw-r--r--tactics/tacsubst.ml48
22 files changed, 379 insertions, 518 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8db7de46c..618450155 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -410,7 +410,7 @@ let _ =
Vernacinterp.vinterp_add "PrintConstr"
(function
[c] when genarg_tag c = ConstrArgType && true ->
- let c = out_gen rawwit_constr c in
+ let c = out_gen (rawwit wit_constr) c in
(fun () -> in_current_context constr_display c)
| _ -> failwith "Vernac extension: cannot occur")
with
@@ -427,7 +427,7 @@ let _ =
Vernacinterp.vinterp_add "PrintPureConstr"
(function
[c] when genarg_tag c = ConstrArgType && true ->
- let c = out_gen rawwit_constr c in
+ let c = out_gen (rawwit wit_constr) c in
(fun () -> in_current_context print_pure_constr c)
| _ -> failwith "Vernac extension: cannot occur")
with
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 0959bfcc1..e3ee3db40 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -16,66 +16,16 @@ open Compat
let loc = CompatLoc.ghost
let default_loc = <:expr< Loc.ghost >>
-let mk_extraarg prefix s =
+let mk_extraarg s =
if Extrawit.tactic_genarg_level s = None then
- <:expr< $lid:prefix^s$ >>
+ <:expr< $lid:"wit_"^s$ >>
else
<:expr<
let module WIT = struct
open Extrawit;
- value wit = $lid:prefix^s$;
+ value wit = $lid:"wit_"^s$;
end in WIT.wit >>
-let rec make_rawwit loc = function
- | BoolArgType -> <:expr< Genarg.rawwit_bool >>
- | IntArgType -> <:expr< Genarg.rawwit_int >>
- | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >>
- | StringArgType -> <:expr< Genarg.rawwit_string >>
- | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
- | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
- | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >>
- | VarArgType -> <:expr< Genarg.rawwit_var >>
- | RefArgType -> <:expr< Genarg.rawwit_ref >>
- | SortArgType -> <:expr< Genarg.rawwit_sort >>
- | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
- | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
- | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
- | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
- | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
- | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
- | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
- | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
- | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >>
- | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
- | PairArgType (t1,t2) ->
- <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >>
- | ExtraArgType s -> mk_extraarg "rawwit_" s
-
-let rec make_globwit loc = function
- | BoolArgType -> <:expr< Genarg.globwit_bool >>
- | IntArgType -> <:expr< Genarg.globwit_int >>
- | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >>
- | StringArgType -> <:expr< Genarg.globwit_string >>
- | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
- | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
- | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >>
- | VarArgType -> <:expr< Genarg.globwit_var >>
- | RefArgType -> <:expr< Genarg.globwit_ref >>
- | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
- | SortArgType -> <:expr< Genarg.globwit_sort >>
- | ConstrArgType -> <:expr< Genarg.globwit_constr >>
- | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
- | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
- | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
- | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
- | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
- | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
- | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >>
- | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >>
- | PairArgType (t1,t2) ->
- <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >>
- | ExtraArgType s -> mk_extraarg "globwit_" s
-
let rec make_wit loc = function
| BoolArgType -> <:expr< Genarg.wit_bool >>
| IntArgType -> <:expr< Genarg.wit_int >>
@@ -99,7 +49,11 @@ let rec make_wit loc = function
| OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
| PairArgType (t1,t2) ->
<:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
- | ExtraArgType s -> mk_extraarg "wit_" s
+ | ExtraArgType s -> mk_extraarg s
+
+let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
+let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
+let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
let has_extraarg =
List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
@@ -131,7 +85,7 @@ let possibly_empty_subentries loc (prods,act) =
| GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
(* We check at runtime if extraarg s parses "epsilon" *)
let s = match p with None -> "_" | Some id -> Names.Id.to_string id in
- <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with
+ <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
[ None -> raise Exit
| Some v -> v ] in $aux tl$ >>
| _ -> assert false (* already filtered out *) in
@@ -201,7 +155,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
Tacinterp.interp_genarg ist gl
(Genarg.in_gen $make_globwit loc globtyp$ x)
in
- (sigma , out_gen $make_wit loc globtyp$ a_interp)>>
+ (sigma , out_gen $make_topwit loc globtyp$ a_interp)>>
| Some f -> <:expr< $lid:f$>> in
let substitute = match h with
| None ->
@@ -212,13 +166,14 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
| Some f -> <:expr< $lid:f$>> in
let se = mlexpr_of_string s in
let wit = <:expr< $lid:"wit_"^s$ >> in
- let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
- let globwit = <:expr< $lid:"globwit_"^s$ >> in
+ let rawwit = <:expr< Genarg.rawwit $wit$ >> in
+ let globwit = <:expr< Genarg.glbwit $wit$ >> in
+ let topwit = <:expr< Genarg.topwit $wit$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
declare_str_items loc
[ <:str_item<
- value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
+ value ($lid:"wit_"^s$) =
Genarg.create_arg $default_value$ $se$>>;
<:str_item<
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
@@ -229,41 +184,37 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
Tacinterp.add_interp_genarg $se$
(fun ist gl x ->
let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in
- (sigma , Genarg.in_gen $wit$ a_interp));
+ (sigma , Genarg.in_gen $topwit$ a_interp));
Tacsubst.add_genarg_subst $se$
(fun subst x ->
(Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))));
Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
(None, [(None, None, $rules$)]);
Pptactic.declare_extra_genarg_pprule
- ($rawwit$, $lid:rawpr$)
- ($globwit$, $lid:globpr$)
- ($wit$, $lid:pr$) }
+ $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ }
>> ]
let declare_vernac_argument loc s pr cl =
let se = mlexpr_of_string s in
let wit = <:expr< $lid:"wit_"^s$ >> in
- let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
- let globwit = <:expr< $lid:"globwit_"^s$ >> in
+ let rawwit = <:expr< Genarg.rawwit $wit$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
let pr_rules = match pr with
| None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
| Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
declare_str_items loc
[ <:str_item<
- value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
- ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
- $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>;
+ value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
+ Genarg.create_arg None $se$ >>;
<:str_item<
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
<:str_item< do {
Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
(None, [(None, None, $rules$)]);
- Pptactic.declare_extra_genarg_pprule
- ($rawwit$, $pr_rules$)
- ($globwit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer"))
- ($wit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
+ Pptactic.declare_extra_genarg_pprule $wit$
+ $pr_rules$
+ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer"))
+ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
>> ]
open Pcoq
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 6e62504a3..1b29da681 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -44,7 +44,7 @@ let rec make_let e = function
let p = Names.Id.to_string p in
let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
let e = make_let e l in
- let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
+ let v = <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in
<:expr< let $lid:p$ = $v$ in $e$ >>
| _::l -> make_let e l
@@ -74,7 +74,7 @@ let rec make_args = function
| GramNonTerminal(loc,t,_,Some p)::l ->
let loc = of_coqloc loc in
let p = Names.Id.to_string p in
- <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
+ <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
| _::l -> make_args l
let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
@@ -124,8 +124,9 @@ let rec possibly_empty_subentries loc = function
OptArgType _|
ExtraArgType _ as t),_,_)->
(* This possibly parses epsilon *)
+ let wit = make_wit loc t in
let rawwit = make_rawwit loc t in
- <:expr< match Genarg.default_empty_value $rawwit$ with
+ <:expr< match Genarg.default_empty_value $wit$ with
[ None -> failwith ""
| Some v ->
Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
diff --git a/interp/genarg.ml b/interp/genarg.ml
index a029a3b31..5d61de508 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -74,6 +74,11 @@ type open_glob_constr = unit * glob_constr_and_expr
type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern
+type ('raw, 'glob, 'top) genarg_type = argument_type
+
+type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
+(** Alias for concision *)
+
(* Dynamics but tagged by a type expression *)
type 'a generic_argument = argument_type * Obj.t
@@ -82,88 +87,50 @@ type rlevel
type glevel
type tlevel
-let rawwit_bool = BoolArgType
-let globwit_bool = BoolArgType
+let rawwit t = t
+let glbwit t = t
+let topwit t = t
+
let wit_bool = BoolArgType
-let rawwit_int = IntArgType
-let globwit_int = IntArgType
let wit_int = IntArgType
-let rawwit_int_or_var = IntOrVarArgType
-let globwit_int_or_var = IntOrVarArgType
let wit_int_or_var = IntOrVarArgType
-let rawwit_string = StringArgType
-let globwit_string = StringArgType
let wit_string = StringArgType
-let rawwit_pre_ident = PreIdentArgType
-let globwit_pre_ident = PreIdentArgType
let wit_pre_ident = PreIdentArgType
-let rawwit_intro_pattern = IntroPatternArgType
-let globwit_intro_pattern = IntroPatternArgType
let wit_intro_pattern = IntroPatternArgType
-let rawwit_ident_gen b = IdentArgType b
-let globwit_ident_gen b = IdentArgType b
let wit_ident_gen b = IdentArgType b
-let rawwit_ident = rawwit_ident_gen true
-let globwit_ident = globwit_ident_gen true
let wit_ident = wit_ident_gen true
-let rawwit_pattern_ident = rawwit_ident_gen false
-let globwit_pattern_ident = globwit_ident_gen false
let wit_pattern_ident = wit_ident_gen false
-let rawwit_var = VarArgType
-let globwit_var = VarArgType
let wit_var = VarArgType
-let rawwit_ref = RefArgType
-let globwit_ref = RefArgType
let wit_ref = RefArgType
-let rawwit_quant_hyp = QuantHypArgType
-let globwit_quant_hyp = QuantHypArgType
let wit_quant_hyp = QuantHypArgType
-let rawwit_sort = SortArgType
-let globwit_sort = SortArgType
let wit_sort = SortArgType
-let rawwit_constr = ConstrArgType
-let globwit_constr = ConstrArgType
let wit_constr = ConstrArgType
-let rawwit_constr_may_eval = ConstrMayEvalArgType
-let globwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType
-let rawwit_open_constr_gen b = OpenConstrArgType b
-let globwit_open_constr_gen b = OpenConstrArgType b
let wit_open_constr_gen b = OpenConstrArgType b
-let rawwit_open_constr = rawwit_open_constr_gen false
-let globwit_open_constr = globwit_open_constr_gen false
let wit_open_constr = wit_open_constr_gen false
-let rawwit_casted_open_constr = rawwit_open_constr_gen true
-let globwit_casted_open_constr = globwit_open_constr_gen true
let wit_casted_open_constr = wit_open_constr_gen true
-let rawwit_constr_with_bindings = ConstrWithBindingsArgType
-let globwit_constr_with_bindings = ConstrWithBindingsArgType
let wit_constr_with_bindings = ConstrWithBindingsArgType
-let rawwit_bindings = BindingsArgType
-let globwit_bindings = BindingsArgType
let wit_bindings = BindingsArgType
-let rawwit_red_expr = RedExprArgType
-let globwit_red_expr = RedExprArgType
let wit_red_expr = RedExprArgType
let wit_list0 t = List0ArgType t
@@ -242,9 +209,7 @@ let create_arg v s =
Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s));
let t = ExtraArgType s in
dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
- (t,t,t)
-
-let exists_argtype s = List.mem_assoc s !dyntab
+ t
let default_empty_argtype_value s = List.assoc s !dyntab
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 7bcb5aa11..0f6ffddd9 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -92,120 +92,116 @@ ExtraArgType of string '_a '_b
{% \end{%}verbatim{% }%}
*)
-(** All of [rlevel], [glevel] and [tlevel] must be non convertible
- to ensure the injectivity of the type inference from type
- ['co generic_argument] to [('a,'co) abstract_argument_type];
- this guarantees that, for 'co fixed, the type of
- out_gen is monomorphic over 'a, hence type-safe
-*)
+(** {5 Base type combinators} *)
-type rlevel
-type glevel
-type tlevel
+type ('raw, 'glob, 'top) genarg_type
+(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
+ one, and ['top] the internalized one. *)
+
+type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
+(** Alias for concision when the three types agree. *)
+
+val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+(** Create a new generic type of argument: force to associate
+ unique ML types at each of the three levels. *)
+
+(** {6 Type constructors} *)
+
+val wit_bool : bool uniform_genarg_type
+
+val wit_int : int uniform_genarg_type
-type ('a,'co) abstract_argument_type
+val wit_int_or_var : int or_var uniform_genarg_type
-val rawwit_bool : (bool,rlevel) abstract_argument_type
-val globwit_bool : (bool,glevel) abstract_argument_type
-val wit_bool : (bool,tlevel) abstract_argument_type
+val wit_string : string uniform_genarg_type
-val rawwit_int : (int,rlevel) abstract_argument_type
-val globwit_int : (int,glevel) abstract_argument_type
-val wit_int : (int,tlevel) abstract_argument_type
+val wit_pre_ident : string uniform_genarg_type
-val rawwit_int_or_var : (int or_var,rlevel) abstract_argument_type
-val globwit_int_or_var : (int or_var,glevel) abstract_argument_type
-val wit_int_or_var : (int or_var,tlevel) abstract_argument_type
+val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
-val rawwit_string : (string,rlevel) abstract_argument_type
-val globwit_string : (string,glevel) abstract_argument_type
+val wit_ident : Id.t uniform_genarg_type
-val wit_string : (string,tlevel) abstract_argument_type
+val wit_pattern_ident : Id.t uniform_genarg_type
-val rawwit_pre_ident : (string,rlevel) abstract_argument_type
-val globwit_pre_ident : (string,glevel) abstract_argument_type
-val wit_pre_ident : (string,tlevel) abstract_argument_type
+val wit_ident_gen : bool -> Id.t uniform_genarg_type
-val rawwit_intro_pattern : (intro_pattern_expr located,rlevel) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr located,glevel) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr located,tlevel) abstract_argument_type
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-val rawwit_ident : (Id.t,rlevel) abstract_argument_type
-val globwit_ident : (Id.t,glevel) abstract_argument_type
-val wit_ident : (Id.t,tlevel) abstract_argument_type
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-val rawwit_pattern_ident : (Id.t,rlevel) abstract_argument_type
-val globwit_pattern_ident : (Id.t,glevel) abstract_argument_type
-val wit_pattern_ident : (Id.t,tlevel) abstract_argument_type
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-val rawwit_ident_gen : bool -> (Id.t,rlevel) abstract_argument_type
-val globwit_ident_gen : bool -> (Id.t,glevel) abstract_argument_type
-val wit_ident_gen : bool -> (Id.t,tlevel) abstract_argument_type
+val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-val rawwit_var : (Id.t located,rlevel) abstract_argument_type
-val globwit_var : (Id.t located,glevel) abstract_argument_type
-val wit_var : (Id.t,tlevel) abstract_argument_type
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-val rawwit_ref : (reference,rlevel) abstract_argument_type
-val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type
-val wit_ref : (global_reference,tlevel) abstract_argument_type
+val wit_constr_may_eval :
+ ((constr_expr,reference or_by_notation,constr_expr) may_eval,
+ (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
+ constr) genarg_type
-val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-val rawwit_sort : (glob_sort,rlevel) abstract_argument_type
-val globwit_sort : (glob_sort,glevel) abstract_argument_type
-val wit_sort : (sorts,tlevel) abstract_argument_type
+val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
-val globwit_constr : (glob_constr_and_expr,glevel) abstract_argument_type
-val wit_constr : (constr,tlevel) abstract_argument_type
+val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type
-val globwit_constr_may_eval : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,glevel) abstract_argument_type
-val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
+val wit_constr_with_bindings :
+ (constr_expr with_bindings,
+ glob_constr_and_expr with_bindings,
+ constr with_bindings sigma) genarg_type
-val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type
+val wit_bindings :
+ (constr_expr bindings,
+ glob_constr_and_expr bindings,
+ constr bindings sigma) genarg_type
-val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type
-val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type
-val wit_open_constr : (open_constr,tlevel) abstract_argument_type
+val wit_red_expr :
+ ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+ (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type
-val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type
-val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
+val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
+ ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
-val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
-val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type
+(** {5 Specialized types} *)
-val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
-val globwit_bindings : (glob_constr_and_expr bindings,glevel) abstract_argument_type
-val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type
+(** All of [rlevel], [glevel] and [tlevel] must be non convertible
+ to ensure the injectivity of the type inference from type
+ ['co generic_argument] to [('a,'co) abstract_argument_type];
+ this guarantees that, for 'co fixed, the type of
+ out_gen is monomorphic over 'a, hence type-safe
+*)
+
+type rlevel
+type glevel
+type tlevel
-val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type
-val globwit_red_expr : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type
+type ('a, 'co) abstract_argument_type
+(** Type at level ['co] represented by an OCaml value of type ['a]. *)
-val wit_list0 :
- ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
+val rawwit : ('a, 'b, 'c) genarg_type -> ('a, 'co) abstract_argument_type
+(** Projection on the raw type constructor. *)
-val wit_list1 :
- ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
+val glbwit : ('a, 'b, 'c) genarg_type -> ('b, 'co) abstract_argument_type
+(** Projection on the globalized type constructor. *)
-val wit_opt :
- ('a,'co) abstract_argument_type -> ('a option,'co) abstract_argument_type
+val topwit : ('a, 'b, 'c) genarg_type -> ('c, 'co) abstract_argument_type
+(** Projection on the internalized type constructor. *)
-val wit_pair :
- ('a,'co) abstract_argument_type ->
- ('b,'co) abstract_argument_type ->
- ('a * 'b,'co) abstract_argument_type
+(** {5 Generic arguments} *)
-(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
type 'a generic_argument
+(** A inhabitant of ['level generic_argument] is a inhabitant of some type at
+ level ['level], together with the representation of this type. *)
+
+(** {6 Manipulation of generic arguments}
+
+Those functions fail if they are applied to an argument which has not the right
+dynamic type. *)
val fold_list0 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
@@ -237,16 +233,6 @@ val app_pair :
('a generic_argument -> 'b generic_argument)
-> 'a generic_argument -> 'b generic_argument
-(** create a new generic type of argument: force to associate
- unique ML types at each of the three levels *)
-val create_arg : 'rawa option ->
- string ->
- ('a,tlevel) abstract_argument_type
- * ('globa,glevel) abstract_argument_type
- * ('rawa,rlevel) abstract_argument_type
-
-val exists_argtype : string -> bool
-
type argument_type =
(** Basic types *)
| BoolArgType
@@ -298,4 +284,4 @@ type an_arg_of_this_type
val in_generic :
argument_type -> an_arg_of_this_type -> 'co generic_argument
-val default_empty_value : ('a,rlevel) abstract_argument_type -> 'a option
+val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index b36e39079..8332bd49f 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -15,12 +15,12 @@ open Genarg
let tactic_main_level = 5
-let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg None "tactic0"
-let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg None "tactic1"
-let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg None "tactic2"
-let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg None "tactic3"
-let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg None "tactic4"
-let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg None "tactic5"
+let wit_tactic0 = create_arg None "tactic0"
+let wit_tactic1 = create_arg None "tactic1"
+let wit_tactic2 = create_arg None "tactic2"
+let wit_tactic3 = create_arg None "tactic3"
+let wit_tactic4 = create_arg None "tactic4"
+let wit_tactic5 = create_arg None "tactic5"
let wit_tactic = function
| 0 -> wit_tactic0
@@ -31,24 +31,6 @@ let wit_tactic = function
| 5 -> wit_tactic5
| n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
-let globwit_tactic = function
- | 0 -> globwit_tactic0
- | 1 -> globwit_tactic1
- | 2 -> globwit_tactic2
- | 3 -> globwit_tactic3
- | 4 -> globwit_tactic4
- | 5 -> globwit_tactic5
- | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
-
-let rawwit_tactic = function
- | 0 -> rawwit_tactic0
- | 1 -> rawwit_tactic1
- | 2 -> rawwit_tactic2
- | 3 -> rawwit_tactic3
- | 4 -> rawwit_tactic4
- | 5 -> rawwit_tactic5
- | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n)
-
let tactic_genarg_level s =
if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then
let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index c7795bb11..a74c8a259 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -15,33 +15,14 @@ open Tacexpr
val tactic_main_level : int
-val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type
-
-val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type
-val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type
-val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type
+val wit_tactic : int -> (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+
+val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
val is_tactic_genarg : argument_type -> bool
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 20fe3af64..95ffd281c 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -55,9 +55,7 @@ GEXTEND Gram
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
-let (wit_withtac : Genarg.tlevel withtac_argtype),
- (globwit_withtac : Genarg.glevel withtac_argtype),
- (rawwit_withtac : Genarg.rlevel withtac_argtype) =
+let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
Genarg.create_arg None "withtac"
open Obligations
@@ -138,7 +136,4 @@ let () =
in
(* should not happen *)
let dummy _ _ _ expr = assert false in
- Pptactic.declare_extra_genarg_pprule
- (rawwit_withtac, printer)
- (globwit_withtac, dummy)
- (wit_withtac, dummy)
+ Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 28c64c147..3c04503dd 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -286,7 +286,7 @@ let create_entry (u, utab) s etyp =
new_entry etyp (u, utab) s
let create_constr_entry s =
- outGramObj rawwit_constr (create_entry uconstr s ConstrArgType)
+ outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
let create_generic_entry s wit =
outGramObj wit (create_entry utactic s (unquote wit))
@@ -306,22 +306,22 @@ module Prim =
(* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic or vernac extensions *)
- let preident = gec_gen rawwit_pre_ident "preident"
- let ident = gec_gen rawwit_ident "ident"
- let natural = gec_gen rawwit_int "natural"
- let integer = gec_gen rawwit_int "integer"
+ let preident = gec_gen (rawwit wit_pre_ident) "preident"
+ let ident = gec_gen (rawwit wit_ident) "ident"
+ let natural = gec_gen (rawwit wit_int) "natural"
+ let integer = gec_gen (rawwit wit_int) "integer"
let bigint = Gram.entry_create "Prim.bigint"
- let string = gec_gen rawwit_string "string"
- let reference = make_gen_entry uprim rawwit_ref "reference"
+ let string = gec_gen (rawwit wit_string) "string"
+ let reference = make_gen_entry uprim (rawwit wit_ref) "reference"
let by_notation = Gram.entry_create "by_notation"
let smart_global = Gram.entry_create "smart_global"
(* parsed like ident but interpreted as a term *)
- let var = gec_gen rawwit_var "var"
+ let var = gec_gen (rawwit wit_var) "var"
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
- let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident"
+ let pattern_ident = gec_gen (rawwit wit_pattern_ident) "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
@@ -338,7 +338,7 @@ module Prim =
module Constr =
struct
- let gec_constr = make_gen_entry uconstr rawwit_constr
+ let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
(* Entries that can be refered via the string -> Gram.entry table *)
let constr = gec_constr "constr"
@@ -346,9 +346,9 @@ module Constr =
let constr_eoi = eoi_entry constr
let lconstr = gec_constr "lconstr"
let binder_constr = create_constr_entry "binder_constr"
- let ident = make_gen_entry uconstr rawwit_ident "ident"
- let global = make_gen_entry uconstr rawwit_ref "global"
- let sort = make_gen_entry uconstr rawwit_sort "sort"
+ let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
+ let global = make_gen_entry uconstr (rawwit wit_ref) "global"
+ let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
@@ -376,27 +376,27 @@ module Tactic =
(* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
+ make_gen_entry utactic (rawwit (wit_open_constr_gen false)) "open_constr"
let casted_open_constr =
- make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr"
+ make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr"
let constr_with_bindings =
- make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
+ make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
let bindings =
- make_gen_entry utactic rawwit_bindings "bindings"
- let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval"
+ make_gen_entry utactic (rawwit wit_bindings) "bindings"
+ let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
let quantified_hypothesis =
- make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
- let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
- let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr"
+ make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis"
+ let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var"
+ let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
let simple_intropattern =
- make_gen_entry utactic rawwit_intro_pattern "simple_intropattern"
+ make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
(* Main entries for ltac *)
let tactic_arg = Gram.entry_create "tactic:tactic_arg"
let tactic_expr = Gram.entry_create "tactic:tactic_expr"
let binder_tactic = Gram.entry_create "tactic:binder_tactic"
- let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
+ let tactic = make_gen_entry utactic (rawwit (wit_tactic tactic_main_level)) "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 70338c52b..291fabdb6 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -100,27 +100,25 @@ let proof_instr = Gram.entry_create "proofmode:instr"
(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
(* [Genarg.create_arg] creates a new embedding into Genarg. *)
-let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
+let wit_proof_instr =
Genarg.create_arg None "proof_instr"
let _ = Tacintern.add_intern_genarg "proof_instr"
begin fun e x -> (* declares the globalisation function *)
- Genarg.in_gen globwit_proof_instr
- (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x))
+ Genarg.in_gen (Genarg.glbwit wit_proof_instr)
+ (Decl_interp.intern_proof_instr e (Genarg.out_gen (Genarg.rawwit wit_proof_instr) x))
end
let _ = Tacinterp.add_interp_genarg "proof_instr"
begin fun ist gl x -> (* declares the interpretation function *)
Tacmach.project gl ,
- Genarg.in_gen wit_proof_instr
- (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x))
+ Genarg.in_gen (Genarg.topwit wit_proof_instr)
+ (interp_proof_instr ist gl (Genarg.out_gen (Genarg.glbwit wit_proof_instr) x))
end
(* declares the substitution function, irrelevant in our case : *)
let _ = Tacsubst.add_genarg_subst "proof_instr" (fun _ x -> x)
-let _ = Pptactic.declare_extra_genarg_pprule
- (rawwit_proof_instr, pr_raw_proof_instr)
- (globwit_proof_instr, pr_glob_proof_instr)
- (wit_proof_instr, pr_proof_instr)
+let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
+ pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
(* We use the VERNAC EXTEND facility with a custom non-terminal
to populate [proof_mode] with a new toplevel interpreter.
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 088b4a0cd..8b90824fd 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -151,11 +151,9 @@ GEXTEND Gram
;
END
-type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type
+type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
-let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
- (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
- (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
+let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
Genarg.create_arg None "function_rec_definition_loc"
VERNAC COMMAND EXTEND Function
["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index b6b69ec2d..5556912eb 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -129,8 +129,8 @@ let closed_term_ast l =
let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
TacFun([Some(Id.of_string"t")],
TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
- [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None);
- Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
+ [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
+ Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
diff --git a/printing/ppextra.ml b/printing/ppextra.ml
index f06ebd9d9..8acdd2e1b 100644
--- a/printing/ppextra.ml
+++ b/printing/ppextra.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Genarg
open Ppextend
open Pptactic
open Extrawit
@@ -13,8 +14,7 @@ open Extrawit
let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
let _ = for i=0 to 5 do
- declare_extra_genarg_pprule
- (rawwit_tactic i, pr_tac_polymorphic i)
- (globwit_tactic i, pr_tac_polymorphic i)
- (wit_tactic i, pr_tac_polymorphic i)
+ let wit = wit_tactic i in
+ declare_extra_genarg_pprule wit
+ (pr_tac_polymorphic i) (pr_tac_polymorphic i) (pr_tac_polymorphic i)
done
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 37678525e..35e153e0f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -62,15 +62,15 @@ type 'a extra_genarg_printer =
let genarg_pprule = ref String.Map.empty
-let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
- let s = match unquote wit with
+let declare_extra_genarg_pprule wit f g h =
+ let s = match unquote (topwit wit) with
| ExtraArgType s -> s
| _ -> error
"Can declare a pretty-printing rule only for extra argument types."
in
- let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
- let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
- let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
+ let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in
+ let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in
+ let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
let pr_arg pr x = spc () ++ pr x
@@ -141,29 +141,29 @@ let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
- | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
- | IntArgType -> int (out_gen rawwit_int x)
- | IntOrVarArgType -> pr_or_var int (out_gen rawwit_int_or_var x)
- | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\""
- | PreIdentArgType -> str (out_gen rawwit_pre_ident x)
- | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x)
- | VarArgType -> pr_located pr_id (out_gen rawwit_var x)
- | RefArgType -> prref (out_gen rawwit_ref x)
- | SortArgType -> pr_glob_sort (out_gen rawwit_sort x)
- | ConstrArgType -> prc (out_gen rawwit_constr x)
+ | BoolArgType -> str (if out_gen (rawwit wit_bool) x then "true" else "false")
+ | IntArgType -> int (out_gen (rawwit wit_int) x)
+ | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
+ | StringArgType -> str "\"" ++ str (out_gen (rawwit wit_string) x) ++ str "\""
+ | PreIdentArgType -> str (out_gen (rawwit wit_pre_ident) x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen (rawwit wit_intro_pattern) x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
+ | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
+ | RefArgType -> prref (out_gen (rawwit wit_ref) x)
+ | SortArgType -> pr_glob_sort (out_gen (rawwit wit_sort) x)
+ | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
| ConstrMayEvalArgType ->
pr_may_eval prc prlc (pr_or_by_notation prref) prpat
- (out_gen rawwit_constr_may_eval x)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
+ (out_gen (rawwit wit_constr_may_eval) x)
+ | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
- (out_gen rawwit_red_expr x)
- | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x))
+ (out_gen (rawwit wit_red_expr) x)
+ | OpenConstrArgType b -> prc (snd (out_gen (rawwit (wit_open_constr_gen b)) x))
| ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x)
+ pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
| BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen rawwit_bindings x)
+ pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
| List0ArgType _ ->
hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
(fold_list0 (fun a l -> a::l) x []))
@@ -184,32 +184,32 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
let rec pr_glob_generic prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
- | IntArgType -> int (out_gen globwit_int x)
- | IntOrVarArgType -> pr_or_var int (out_gen globwit_int_or_var x)
- | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\""
- | PreIdentArgType -> str (out_gen globwit_pre_ident x)
- | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x)
- | VarArgType -> pr_located pr_id (out_gen globwit_var x)
- | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x)
- | SortArgType -> pr_glob_sort (out_gen globwit_sort x)
- | ConstrArgType -> prc (out_gen globwit_constr x)
+ | BoolArgType -> str (if out_gen (glbwit wit_bool) x then "true" else "false")
+ | IntArgType -> int (out_gen (glbwit wit_int) x)
+ | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
+ | StringArgType -> str "\"" ++ str (out_gen (glbwit wit_string) x) ++ str "\""
+ | PreIdentArgType -> str (out_gen (glbwit wit_pre_ident) x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen (glbwit wit_intro_pattern) x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
+ | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
+ | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
+ | SortArgType -> pr_glob_sort (out_gen (glbwit wit_sort) x)
+ | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
| ConstrMayEvalArgType ->
pr_may_eval prc prlc
(pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
- (out_gen globwit_constr_may_eval x)
+ (out_gen (glbwit wit_constr_may_eval) x)
| QuantHypArgType ->
- pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
+ pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
| RedExprArgType ->
pr_red_expr
(prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
- (out_gen globwit_red_expr x)
- | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x))
+ (out_gen (glbwit wit_red_expr) x)
+ | OpenConstrArgType b -> prc (snd (out_gen (glbwit (wit_open_constr_gen b)) x))
| ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x)
+ pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
| BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen globwit_bindings x)
+ pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
| List0ArgType _ ->
hov 0 (pr_sequence (pr_glob_generic prc prlc prtac prpat)
(fold_list0 (fun a l -> a::l) x []))
@@ -228,28 +228,28 @@ let rec pr_glob_generic prc prlc prtac prpat x =
let rec pr_generic prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
- | IntArgType -> int (out_gen wit_int x)
- | IntOrVarArgType -> pr_or_var int (out_gen wit_int_or_var x)
- | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\""
- | PreIdentArgType -> str (out_gen wit_pre_ident x)
- | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x)
- | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x)
- | VarArgType -> pr_id (out_gen wit_var x)
- | RefArgType -> pr_global (out_gen wit_ref x)
- | SortArgType -> pr_sort (out_gen wit_sort x)
- | ConstrArgType -> prc (out_gen wit_constr x)
- | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x)
+ | BoolArgType -> str (if out_gen (topwit wit_bool) x then "true" else "false")
+ | IntArgType -> int (out_gen (topwit wit_int) x)
+ | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
+ | StringArgType -> str "\"" ++ str (out_gen (topwit wit_string) x) ++ str "\""
+ | PreIdentArgType -> str (out_gen (topwit wit_pre_ident) x)
+ | IntroPatternArgType -> pr_intro_pattern (out_gen (topwit wit_intro_pattern) x)
+ | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
+ | VarArgType -> pr_id (out_gen (topwit wit_var) x)
+ | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
+ | SortArgType -> pr_sort (out_gen (topwit wit_sort) x)
+ | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
+ | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
+ | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
- (out_gen wit_red_expr x)
- | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
+ (out_gen (topwit wit_red_expr) x)
+ | OpenConstrArgType b -> prc (snd (out_gen (topwit (wit_open_constr_gen b)) x))
| ConstrWithBindingsArgType ->
- let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in
+ let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
pr_with_bindings prc prlc (c,b)
| BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it
+ pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
| List0ArgType _ ->
hov 0 (pr_sequence (pr_generic prc prlc prtac prpat)
(fold_list0 (fun a l -> a::l) x []))
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 795f2e4fd..277676ae4 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -39,11 +39,11 @@ type 'a extra_genarg_printer =
(tolerability -> glob_tactic_expr -> std_ppcmds) ->
'a -> std_ppcmds
- (** if the boolean is false then the extension applies only to old syntax *)
val declare_extra_genarg_pprule :
- ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) ->
- ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
- ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit
+ ('a, 'b, 'c) genarg_type ->
+ 'a raw_extra_genarg_printer ->
+ 'b glob_extra_genarg_printer ->
+ 'c extra_genarg_printer -> unit
type grammar_terminals = string option list
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 709403a48..00f0cd715 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -16,10 +16,14 @@ open Environ
open Explore
val hintbases : hint_db_name list option Pcoq.Gram.entry
-val wit_hintbases : hint_db_name list option typed_abstract_argument_type
-val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
-val rawwit_auto_using : Genarg.open_constr_expr list raw_abstract_argument_type
+val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type
+
+val wit_auto_using :
+ (Genarg.open_constr_expr list,
+ Genarg.open_glob_constr list, Evd.open_constr list)
+ Genarg.genarg_type
+
val e_assumption : tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index a15f907c6..21e120a7e 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -283,13 +283,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
(* spiwack argument for the commands of the retroknowledge *)
-let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
+let wit_r_nat_field =
Genarg.create_arg None "r_nat_field"
-let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
+let wit_r_n_field =
Genarg.create_arg None "r_n_field"
-let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
+let wit_r_int31_field =
Genarg.create_arg None "r_int31_field"
-let (wit_r_field, globwit_r_field, rawwit_r_field) =
+let wit_r_field =
Genarg.create_arg None "r_field"
(* spiwack: the print functions are incomplete, but I don't know what they are
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7fc3ac8a5..cd4d777d6 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,20 +15,19 @@ open Termops
open Glob_term
open Misctypes
-val rawwit_orient : bool raw_abstract_argument_type
-val globwit_orient : bool glob_abstract_argument_type
-val wit_orient : bool typed_abstract_argument_type
+val wit_orient : bool Genarg.uniform_genarg_type
val orient : bool Pcoq.Gram.entry
val pr_orient : bool -> Pp.std_ppcmds
val occurrences : (int list or_var) Pcoq.Gram.entry
-val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
-val wit_occurrences : (int list) typed_abstract_argument_type
+val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
val pr_occurrences : int list or_var -> Pp.std_ppcmds
val occurrences_of : int list -> Locus.occurrences
-val rawwit_glob : constr_expr raw_abstract_argument_type
-val wit_glob : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type
+val wit_glob :
+ (constr_expr,
+ Genarg.glob_constr_and_expr,
+ Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
val glob : constr_expr Pcoq.Gram.entry
type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -36,22 +35,27 @@ type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
type loc_place = Id.t Loc.located gen_place
type place = Id.t gen_place
-val rawwit_hloc : loc_place raw_abstract_argument_type
-val wit_hloc : place typed_abstract_argument_type
+val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
val hloc : loc_place Pcoq.Gram.entry
val pr_hloc : loc_place -> Pp.std_ppcmds
val in_arg_hyp: (Names.Id.t Loc.located list option * bool) Pcoq.Gram.entry
-val globwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) glob_abstract_argument_type
-val rawwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) raw_abstract_argument_type
-val wit_in_arg_hyp : (Names.Id.t list option * bool) typed_abstract_argument_type
+
+val wit_in_arg_hyp :
+ ((Names.Id.t Loc.located list option * bool),
+ (Names.Id.t Loc.located list option * bool),
+ (Names.Id.t list option * bool)) Genarg.genarg_type
+
val raw_in_arg_hyp_to_clause : (Names.Id.t Loc.located list option * bool) -> Locus.clause
val glob_in_arg_hyp_to_clause : (Names.Id.t list option * bool) -> Locus.clause
val pr_in_arg_hyp : (Names.Id.t list option * bool) -> Pp.std_ppcmds
val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
-val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type
-val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
+val wit_by_arg_tac :
+ (raw_tactic_expr option,
+ glob_tactic_expr option,
+ glob_tactic_expr option) Genarg.genarg_type
+
val pr_by_arg_tac :
(int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
raw_tactic_expr option -> Pp.std_ppcmds
@@ -60,5 +64,4 @@ val pr_by_arg_tac :
(** Spiwack: Primitive for retroknowledge registration *)
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
-val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type
-val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type
+val wit_retroknowledge_field : Retroknowledge.field Genarg.uniform_genarg_type
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f7c13d01a..0e8b5a2db 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1665,13 +1665,10 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
(Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
(Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
-type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+type binders_argtype = local_binder list
-let _, _, rawwit_binders =
- (Genarg.create_arg None "binders" :
- Genarg.tlevel binders_argtype *
- Genarg.glevel binders_argtype *
- Genarg.rlevel binders_argtype)
+let wit_binders =
+ (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
open Pcoq.Constr
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4662494aa..aa91db9b0 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -765,49 +765,49 @@ and intern_match_rule onlytac ist = function
and intern_genarg ist x =
match genarg_tag x with
- | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
- | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
+ | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (rawwit wit_bool) x)
+ | IntArgType -> in_gen (glbwit wit_int) (out_gen (rawwit wit_int) x)
| IntOrVarArgType ->
- in_gen globwit_int_or_var
- (intern_or_var ist (out_gen rawwit_int_or_var x))
+ in_gen (glbwit wit_int_or_var)
+ (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
| StringArgType ->
- in_gen globwit_string (out_gen rawwit_string x)
+ in_gen (glbwit wit_string) (out_gen (rawwit wit_string) x)
| PreIdentArgType ->
- in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
+ in_gen (glbwit wit_pre_ident) (out_gen (rawwit wit_pre_ident) x)
| IntroPatternArgType ->
let lf = ref ([],[]) in
(* how to know which names are bound by the intropattern *)
- in_gen globwit_intro_pattern
- (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
+ in_gen (glbwit wit_intro_pattern)
+ (intern_intro_pattern lf ist (out_gen (rawwit wit_intro_pattern) x))
| IdentArgType b ->
let lf = ref ([],[]) in
- in_gen (globwit_ident_gen b)
- (intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
+ in_gen (glbwit (wit_ident_gen b))
+ (intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
| VarArgType ->
- in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
+ in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
| RefArgType ->
- in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
+ in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
| SortArgType ->
- in_gen globwit_sort (out_gen rawwit_sort x)
+ in_gen (glbwit wit_sort) (out_gen (rawwit wit_sort) x)
| ConstrArgType ->
- in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
+ in_gen (glbwit wit_constr) (intern_constr ist (out_gen (rawwit wit_constr) x))
| ConstrMayEvalArgType ->
- in_gen globwit_constr_may_eval
- (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+ in_gen (glbwit wit_constr_may_eval)
+ (intern_constr_may_eval ist (out_gen (rawwit wit_constr_may_eval) x))
| QuantHypArgType ->
- in_gen globwit_quant_hyp
- (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+ in_gen (glbwit wit_quant_hyp)
+ (intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x))
| RedExprArgType ->
- in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x))
+ in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x))
| OpenConstrArgType b ->
- in_gen (globwit_open_constr_gen b)
- ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
+ in_gen (glbwit (wit_open_constr_gen b))
+ ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x)))
| ConstrWithBindingsArgType ->
- in_gen globwit_constr_with_bindings
- (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+ in_gen (glbwit wit_constr_with_bindings)
+ (intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x))
| BindingsArgType ->
- in_gen globwit_bindings
- (intern_bindings ist (out_gen rawwit_bindings x))
+ in_gen (glbwit wit_bindings)
+ (intern_bindings ist (out_gen (rawwit wit_bindings) x))
| List0ArgType _ -> app_list0 (intern_genarg ist) x
| List1ArgType _ -> app_list1 (intern_genarg ist) x
| OptArgType _ -> app_opt (intern_genarg ist) x
@@ -816,8 +816,8 @@ and intern_genarg ist x =
match tactic_genarg_level s with
| Some n ->
(* Special treatment of tactic arguments *)
- in_gen (globwit_tactic n) (intern_tactic_or_tacarg ist
- (out_gen (rawwit_tactic n) x))
+ in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist
+ (out_gen (rawwit (wit_tactic n)) x))
| None ->
lookup_intern_genarg s ist x
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c0903c2a9..1458cd73b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1371,63 +1371,63 @@ and interp_genarg ist gl x =
let rec interp_genarg ist gl x =
let gl = { gl with sigma = !evdref } in
match genarg_tag x with
- | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
- | IntArgType -> in_gen wit_int (out_gen globwit_int x)
+ | BoolArgType -> in_gen (topwit wit_bool) (out_gen (glbwit wit_bool) x)
+ | IntArgType -> in_gen (topwit wit_int) (out_gen (glbwit wit_int) x)
| IntOrVarArgType ->
- in_gen wit_int_or_var
- (ArgArg (interp_int_or_var ist (out_gen globwit_int_or_var x)))
+ in_gen (topwit wit_int_or_var)
+ (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
| StringArgType ->
- in_gen wit_string (out_gen globwit_string x)
+ in_gen (topwit wit_string) (out_gen (glbwit wit_string) x)
| PreIdentArgType ->
- in_gen wit_pre_ident (out_gen globwit_pre_ident x)
+ in_gen (topwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
| IntroPatternArgType ->
- in_gen wit_intro_pattern
- (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
+ in_gen (topwit wit_intro_pattern)
+ (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x))
| IdentArgType b ->
- in_gen (wit_ident_gen b)
- (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))
+ in_gen (topwit (wit_ident_gen b))
+ (pf_interp_fresh_ident ist gl (out_gen (glbwit (wit_ident_gen b)) x))
| VarArgType ->
- in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
+ in_gen (topwit wit_var) (interp_hyp ist gl (out_gen (glbwit wit_var) x))
| RefArgType ->
- in_gen wit_ref (pf_interp_reference ist gl (out_gen globwit_ref x))
+ in_gen (topwit wit_ref) (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))
| SortArgType ->
let (sigma,c_interp) =
pf_interp_constr ist gl
- (GSort (dloc,out_gen globwit_sort x), None)
+ (GSort (dloc,out_gen (glbwit wit_sort) x), None)
in
evdref := sigma;
- in_gen wit_sort
+ in_gen (topwit wit_sort)
(destSort c_interp)
| ConstrArgType ->
- let (sigma,c_interp) = pf_interp_constr ist gl (out_gen globwit_constr x) in
+ let (sigma,c_interp) = pf_interp_constr ist gl (out_gen (glbwit wit_constr) x) in
evdref := sigma;
- in_gen wit_constr c_interp
+ in_gen (topwit wit_constr) c_interp
| ConstrMayEvalArgType ->
- let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+ let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
evdref := sigma;
- in_gen wit_constr_may_eval c_interp
+ in_gen (topwit wit_constr_may_eval) c_interp
| QuantHypArgType ->
- in_gen wit_quant_hyp
+ in_gen (topwit wit_quant_hyp)
(interp_declared_or_quantified_hypothesis ist gl
- (out_gen globwit_quant_hyp x))
+ (out_gen (glbwit wit_quant_hyp) x))
| RedExprArgType ->
- let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in
+ let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen (glbwit wit_red_expr) x) in
evdref := sigma;
- in_gen wit_red_expr r_interp
+ in_gen (topwit wit_red_expr) r_interp
| OpenConstrArgType casted ->
let expected_type =
if casted then OfType (pf_concl gl) else WithoutTypeConstraint in
- in_gen (wit_open_constr_gen casted)
+ in_gen (topwit (wit_open_constr_gen casted))
(interp_open_constr ~expected_type
ist (pf_env gl) (project gl)
- (snd (out_gen (globwit_open_constr_gen casted) x)))
+ (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
| ConstrWithBindingsArgType ->
- in_gen wit_constr_with_bindings
+ in_gen (topwit wit_constr_with_bindings)
(pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
- (out_gen globwit_constr_with_bindings x)))
+ (out_gen (glbwit wit_constr_with_bindings) x)))
| BindingsArgType ->
- in_gen wit_bindings
- (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x)))
+ in_gen (topwit wit_bindings)
+ (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
| List0ArgType ConstrArgType ->
let (sigma,v) = interp_genarg_constr_list0 ist gl x in
evdref := sigma;
@@ -1446,9 +1446,9 @@ and interp_genarg ist gl x =
match tactic_genarg_level s with
| Some n ->
(* Special treatment of tactic arguments *)
- in_gen (wit_tactic n)
+ in_gen (topwit (wit_tactic n))
(TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[],
- out_gen (globwit_tactic n) x))))
+ out_gen (glbwit (wit_tactic n)) x))))
| None ->
let (sigma,v) = lookup_interp_genarg s ist gl x in
evdref:=sigma;
@@ -1458,24 +1458,24 @@ and interp_genarg ist gl x =
!evdref , v
and interp_genarg_constr_list0 ist gl x =
- let lc = out_gen (wit_list0 globwit_constr) x in
+ let lc = out_gen (glbwit (wit_list0 wit_constr)) x in
let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
- sigma , in_gen (wit_list0 wit_constr) lc
+ sigma , in_gen (topwit (wit_list0 wit_constr)) lc
and interp_genarg_constr_list1 ist gl x =
- let lc = out_gen (wit_list1 globwit_constr) x in
+ let lc = out_gen (glbwit (wit_list1 wit_constr)) x in
let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
- sigma , in_gen (wit_list1 wit_constr) lc
+ sigma , in_gen (topwit (wit_list1 wit_constr)) lc
and interp_genarg_var_list0 ist gl x =
- let lc = out_gen (wit_list0 globwit_var) x in
+ let lc = out_gen (glbwit (wit_list0 wit_var)) x in
let lc = interp_hyp_list ist gl lc in
- in_gen (wit_list0 wit_var) lc
+ in_gen (topwit (wit_list0 wit_var)) lc
and interp_genarg_var_list1 ist gl x =
- let lc = out_gen (wit_list1 globwit_var) x in
+ let lc = out_gen (glbwit (wit_list1 wit_var)) x in
let lc = interp_hyp_list ist gl lc in
- in_gen (wit_list1 wit_var) lc
+ in_gen (topwit (wit_list1 wit_var)) lc
(* Interprets the Match expressions *)
and interp_match ist g lz constr lmr =
@@ -1885,45 +1885,45 @@ and interp_atomic ist gl tac =
let evdref = ref gl.sigma in
let f x = match genarg_tag x with
| IntArgType ->
- VInteger (out_gen globwit_int x)
+ VInteger (out_gen (glbwit wit_int) x)
| IntOrVarArgType ->
- mk_int_or_var_value ist (out_gen globwit_int_or_var x)
+ mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)
| PreIdentArgType ->
failwith "pre-identifiers cannot be bound"
| IntroPatternArgType ->
VIntroPattern
- (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)))
+ (snd (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x)))
| IdentArgType b ->
value_of_ident (interp_fresh_ident ist env
- (out_gen (globwit_ident_gen b) x))
+ (out_gen (glbwit (wit_ident_gen b)) x))
| VarArgType ->
- mk_hyp_value ist gl (out_gen globwit_var x)
+ mk_hyp_value ist gl (out_gen (glbwit wit_var) x)
| RefArgType ->
VConstr ([],constr_of_global
- (pf_interp_reference ist gl (out_gen globwit_ref x)))
+ (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x)))
| SortArgType ->
- VConstr ([],mkSort (interp_sort (out_gen globwit_sort x)))
+ VConstr ([],mkSort (interp_sort (out_gen (glbwit wit_sort) x)))
| ConstrArgType ->
- let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in
+ let (sigma,v) = mk_constr_value ist gl (out_gen (glbwit wit_constr) x) in
evdref := sigma;
v
| OpenConstrArgType false ->
- let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen globwit_open_constr x)) in
+ let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x)) in
evdref := sigma;
v
| ConstrMayEvalArgType ->
- let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+ let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
evdref := sigma;
VConstr ([],c_interp)
| ExtraArgType s when not (Option.is_empty (tactic_genarg_level s)) ->
(* Special treatment of tactic arguments *)
let (sigma,v) = val_interp ist gl
- (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
+ (out_gen (glbwit (wit_tactic (Option.get (tactic_genarg_level s)))) x)
in
evdref := sigma;
v
| List0ArgType ConstrArgType ->
- let wit = wit_list0 globwit_constr in
+ let wit = glbwit (wit_list0 wit_constr) in
let (sigma,l_interp) =
List.fold_right begin fun c (sigma,acc) ->
let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
@@ -1933,24 +1933,24 @@ and interp_atomic ist gl tac =
evdref := sigma;
VList (l_interp)
| List0ArgType VarArgType ->
- let wit = wit_list0 globwit_var in
+ let wit = glbwit (wit_list0 wit_var) in
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
| List0ArgType IntArgType ->
- let wit = wit_list0 globwit_int in
+ let wit = glbwit (wit_list0 wit_int) in
VList (List.map (fun x -> VInteger x) (out_gen wit x))
| List0ArgType IntOrVarArgType ->
- let wit = wit_list0 globwit_int_or_var in
+ let wit = glbwit (wit_list0 wit_int_or_var) in
VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
| List0ArgType (IdentArgType b) ->
- let wit = wit_list0 (globwit_ident_gen b) in
+ let wit = glbwit (wit_list0 (wit_ident_gen b)) in
let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
VList (List.map mk_ident (out_gen wit x))
| List0ArgType IntroPatternArgType ->
- let wit = wit_list0 globwit_intro_pattern in
+ let wit = glbwit (wit_list0 wit_intro_pattern) in
let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
VList (List.map mk_ipat (out_gen wit x))
| List1ArgType ConstrArgType ->
- let wit = wit_list1 globwit_constr in
+ let wit = glbwit (wit_list1 wit_constr) in
let (sigma, l_interp) =
List.fold_right begin fun c (sigma,acc) ->
let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
@@ -1960,20 +1960,20 @@ and interp_atomic ist gl tac =
evdref:=sigma;
VList l_interp
| List1ArgType VarArgType ->
- let wit = wit_list1 globwit_var in
+ let wit = glbwit (wit_list1 wit_var) in
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
| List1ArgType IntArgType ->
- let wit = wit_list1 globwit_int in
+ let wit = glbwit (wit_list1 wit_int) in
VList (List.map (fun x -> VInteger x) (out_gen wit x))
| List1ArgType IntOrVarArgType ->
- let wit = wit_list1 globwit_int_or_var in
+ let wit = glbwit (wit_list1 wit_int_or_var) in
VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
| List1ArgType (IdentArgType b) ->
- let wit = wit_list1 (globwit_ident_gen b) in
+ let wit = glbwit (wit_list1 (wit_ident_gen b)) in
let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
VList (List.map mk_ident (out_gen wit x))
| List1ArgType IntroPatternArgType ->
- let wit = wit_list1 globwit_intro_pattern in
+ let wit = glbwit (wit_list1 wit_intro_pattern) in
let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
VList (List.map mk_ipat (out_gen wit x))
| StringArgType | BoolArgType
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 1cf4264ea..bb7caf93b 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -300,40 +300,40 @@ and subst_match_rule subst = function
and subst_genarg subst (x:glob_generic_argument) =
match genarg_tag x with
- | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
- | IntArgType -> in_gen globwit_int (out_gen globwit_int x)
- | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
- | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
- | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
+ | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (glbwit wit_bool) x)
+ | IntArgType -> in_gen (glbwit wit_int) (out_gen (glbwit wit_int) x)
+ | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
+ | StringArgType -> in_gen (glbwit wit_string) (out_gen (glbwit wit_string) x)
+ | PreIdentArgType -> in_gen (glbwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
| IntroPatternArgType ->
- in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
+ in_gen (glbwit wit_intro_pattern) (out_gen (glbwit wit_intro_pattern) x)
| IdentArgType b ->
- in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
- | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
+ in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
+ | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
| RefArgType ->
- in_gen globwit_ref (subst_global_reference subst
- (out_gen globwit_ref x))
+ in_gen (glbwit wit_ref) (subst_global_reference subst
+ (out_gen (glbwit wit_ref) x))
| SortArgType ->
- in_gen globwit_sort (out_gen globwit_sort x)
+ in_gen (glbwit wit_sort) (out_gen (glbwit wit_sort) x)
| ConstrArgType ->
- in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x))
+ in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
| ConstrMayEvalArgType ->
- in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
+ in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x))
| QuantHypArgType ->
- in_gen globwit_quant_hyp
+ in_gen (glbwit wit_quant_hyp)
(subst_declared_or_quantified_hypothesis subst
- (out_gen globwit_quant_hyp x))
+ (out_gen (glbwit wit_quant_hyp) x))
| RedExprArgType ->
- in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
+ in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x))
| OpenConstrArgType b ->
- in_gen (globwit_open_constr_gen b)
- ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x)))
+ in_gen (glbwit (wit_open_constr_gen b))
+ ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x)))
| ConstrWithBindingsArgType ->
- in_gen globwit_constr_with_bindings
- (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x))
+ in_gen (glbwit wit_constr_with_bindings)
+ (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x))
| BindingsArgType ->
- in_gen globwit_bindings
- (subst_bindings subst (out_gen globwit_bindings x))
+ in_gen (glbwit wit_bindings)
+ (subst_bindings subst (out_gen (glbwit wit_bindings) x))
| List0ArgType _ -> app_list0 (subst_genarg subst) x
| List1ArgType _ -> app_list1 (subst_genarg subst) x
| OptArgType _ -> app_opt (subst_genarg subst) x
@@ -342,8 +342,8 @@ and subst_genarg subst (x:glob_generic_argument) =
match Extrawit.tactic_genarg_level s with
| Some n ->
(* Special treatment of tactic arguments *)
- in_gen (Extrawit.globwit_tactic n)
- (subst_tactic subst (out_gen (Extrawit.globwit_tactic n) x))
+ in_gen (glbwit (Extrawit.wit_tactic n))
+ (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x))
| None ->
lookup_genarg_subst s subst x
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 11:12:44 +0000