diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:59:02 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:59:02 +0000 |
commit | b23c6c6f1158dc247615ded5867c290f18aab1b9 (patch) | |
tree | f0ed29a89e1672fa29549716f78316bf382c8d2c /tactics | |
parent | fafd64a1322205c3c4e3cae0680e03ea341b1cd8 (diff) |
Uniformizing generic argument types.
Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.
This has various advantages:
- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.
Documenting a bit Genarg b.t.w.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/eauto.mli | 10 | ||||
-rw-r--r-- | tactics/extraargs.ml4 | 8 | ||||
-rw-r--r-- | tactics/extraargs.mli | 35 | ||||
-rw-r--r-- | tactics/rewrite.ml4 | 9 | ||||
-rw-r--r-- | tactics/tacintern.ml | 54 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 122 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 48 |
7 files changed, 145 insertions, 141 deletions
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 |