diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 10 | ||||
| -rw-r--r-- | interp/genarg.ml | 12 | ||||
| -rw-r--r-- | interp/genarg.mli | 14 | ||||
| -rw-r--r-- | parsing/argextend.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 9 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 11 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 29 |
12 files changed, 59 insertions, 54 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 3e5d1307c0..6758576370 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -887,7 +887,7 @@ and xlate_tac = | _ -> assert false) | _ -> assert false) | TacExtend (_, "refine", [c]) -> - CT_refine (xlate_formula (out_gen rawwit_casted_open_constr c)) + CT_refine (xlate_formula (snd (out_gen rawwit_open_constr c))) | TacExtend (_,"absurd",[c]) -> CT_absurd (xlate_formula (out_gen rawwit_constr c)) | TacExtend (_,"contradiction",[opt_c]) -> @@ -1237,11 +1237,11 @@ and coerce_genarg_to_TARG x = | TacticArgType -> let t = xlate_tactic (out_gen rawwit_tactic x) in CT_coerce_TACTIC_COM_to_TARG t - | CastedOpenConstrArgType -> + | OpenConstrArgType -> CT_coerce_SCOMMENT_CONTENT_to_TARG (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula - (out_gen - rawwit_casted_open_constr x))) + (snd (out_gen + rawwit_open_constr x)))) | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" | BindingsArgType -> xlate_error "TODO: generic with bindings" | RedExprArgType -> xlate_error "TODO: generic red expr" @@ -1331,7 +1331,7 @@ let coerce_genarg_to_VARG x = | TacticArgType -> let t = xlate_tactic (out_gen rawwit_tactic x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) - | CastedOpenConstrArgType -> xlate_error "TODO: generic open constr" + | OpenConstrArgType -> xlate_error "TODO: generic open constr" | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" | BindingsArgType -> xlate_error "TODO: generic with bindings" | RedExprArgType -> xlate_error "TODO: red expr as generic argument" diff --git a/interp/genarg.ml b/interp/genarg.ml index 91b8c5bf74..3483695ecf 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -34,7 +34,7 @@ type argument_type = | ConstrMayEvalArgType | QuantHypArgType | TacticArgType - | CastedOpenConstrArgType + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType @@ -85,8 +85,8 @@ and pr_case_intro_pattern = function ++ str "]" type open_constr = Evd.evar_map * Term.constr -type open_constr_expr = constr_expr -type open_rawconstr = rawconstr_and_expr +type open_constr_expr = unit * constr_expr +type open_rawconstr = unit * rawconstr_and_expr let rawwit_bool = BoolArgType let globwit_bool = BoolArgType @@ -144,9 +144,9 @@ let rawwit_tactic = TacticArgType let globwit_tactic = TacticArgType let wit_tactic = TacticArgType -let rawwit_casted_open_constr = CastedOpenConstrArgType -let globwit_casted_open_constr = CastedOpenConstrArgType -let wit_casted_open_constr = CastedOpenConstrArgType +let rawwit_open_constr = OpenConstrArgType +let globwit_open_constr = OpenConstrArgType +let wit_open_constr = OpenConstrArgType let rawwit_constr_with_bindings = ConstrWithBindingsArgType let globwit_constr_with_bindings = ConstrWithBindingsArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index 7d4aedff6a..7f01cd6ace 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -25,8 +25,8 @@ type 'a and_short_name = 'a * identifier located option type rawconstr_and_expr = rawconstr * constr_expr option type open_constr = Evd.evar_map * Term.constr -type open_constr_expr = constr_expr -type open_rawconstr = rawconstr_and_expr +type open_constr_expr = unit * constr_expr +type open_rawconstr = unit * rawconstr_and_expr type intro_pattern_expr = | IntroOrAndPattern of case_intro_pattern_expr @@ -70,7 +70,7 @@ ConstrArgType constr_expr constr ConstrMayEvalArgType constr_expr may_eval constr QuantHypArgType quantified_hypothesis quantified_hypothesis TacticArgType raw_tactic_expr tactic -CastedOpenConstrArgType constr_expr open_constr +OpenConstrArgType constr_expr open_constr ConstrBindingsArgType constr_expr with_bindings constr with_bindings List0ArgType of argument_type List1ArgType of argument_type @@ -132,9 +132,9 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type -val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type -val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type -val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type +val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type +val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type +val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type @@ -227,7 +227,7 @@ type argument_type = | ConstrMayEvalArgType | QuantHypArgType | TacticArgType - | CastedOpenConstrArgType + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index df48f5d8de..78128a99d8 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -33,7 +33,7 @@ let rec make_rawwit loc = function | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | TacticArgType -> <:expr< Genarg.rawwit_tactic >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> @@ -59,7 +59,7 @@ let rec make_globwit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.globwit_tactic >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> @@ -85,7 +85,7 @@ let rec make_wit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.wit_tactic >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5ba7d591e5..97f5d46a9d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constrarg bindings constr_with_bindings - quantified_hypothesis red_expr int_or_var castedopenconstr + quantified_hypothesis red_expr int_or_var openconstr simple_intropattern; int_or_var: @@ -96,8 +96,8 @@ GEXTEND Gram | IDENT "Check"; c = constr -> ConstrTypeOf c | c = constr -> ConstrTerm c ] ] ; - castedopenconstr: - [ [ c = constr -> c ] ] + openconstr: + [ [ c = constr -> ((),c) ] ] ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 8930c8dcad..70729ce136 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -109,7 +109,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if not !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var castedopenconstr simple_intropattern; + bindings red_expr int_or_var openconstr simple_intropattern; int_or_var: [ [ n = integer -> Genarg.ArgArg n @@ -128,8 +128,8 @@ GEXTEND Gram | id = METAIDENT -> MetaId (loc,id) ] ] ; - castedopenconstr: - [ [ c = constr -> c ] ] + openconstr: + [ [ c = constr -> ((),c) ] ] ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 081d7aeecc..496b6594d0 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -371,8 +371,8 @@ module Tactic = (* Entries that can be refered via the string -> Gram.Entry.e table *) (* Typically for tactic user extensions *) - let castedopenconstr = - make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr" + let openconstr = + make_gen_entry utactic rawwit_open_constr "openconstr" let constr_with_bindings = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = @@ -418,7 +418,7 @@ let reset_all_grammars () = f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern; f Module.module_expr; f Module.module_type; f Tactic.simple_tactic; - f Tactic.castedopenconstr; + f Tactic.openconstr; f Tactic.constr_with_bindings; f Tactic.bindings; f Tactic.constrarg; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c2f1c0240c..76c23ad20b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -156,7 +156,7 @@ module Module : module Tactic : sig open Rawterm - val castedopenconstr : constr_expr Gram.Entry.e + val openconstr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e val constrarg : (constr_expr,reference) may_eval Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3057e41a41..76c9847efd 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -272,8 +272,7 @@ let rec pr_raw_generic prc prlc prtac prref x = pr_arg (pr_red_expr (prc,prref)) (out_gen rawwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (out_gen rawwit_casted_open_constr x) + | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> @@ -320,8 +319,7 @@ let rec pr_glob_generic prc prlc prtac x = pr_arg (pr_red_expr (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (out_gen globwit_casted_open_constr x) + | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) | BindingsArgType -> @@ -367,8 +365,7 @@ let rec pr_generic prc prlc prtac x = | RedExprArgType -> pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (snd (out_gen wit_casted_open_constr x)) + | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) | BindingsArgType -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e1bb51dd79..a4c58aec97 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -272,7 +272,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.HypArgType -> <:expr< Genarg.HypArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >> + | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6ef79ea752..fd8efc5f91 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -158,8 +158,17 @@ END open Refine +let coerce_to_goal tac (sigma,c) gl = + let env = Tacmach.pf_env gl in + let evars = Evd.create_evar_defs sigma in + let j = Retyping.get_judgment_of env sigma c in + let ccl = Tacmach.pf_concl gl in + let (evars,j) = Coercion.inh_conv_coerce_to Util.dummy_loc env evars j ccl in + let sigma = Evd.evars_of evars in + tac (sigma,Reductionops.nf_evar sigma j.Environ.uj_val) gl + TACTIC EXTEND Refine - [ "Refine" castedopenconstr(c) ] -> [ refine c ] + [ "Refine" openconstr(c) ] -> [ coerce_to_goal refine c ] END let refine_tac = h_refine diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5a33f89f3f..3c4130e791 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -885,9 +885,9 @@ and intern_genarg ist x = in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x)) | TacticArgType -> in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x)) - | CastedOpenConstrArgType -> - in_gen globwit_casted_open_constr - (intern_constr ist (out_gen rawwit_casted_open_constr x)) + | OpenConstrArgType -> + in_gen globwit_open_constr + ((),intern_constr ist (snd (out_gen rawwit_open_constr x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) @@ -1194,20 +1194,19 @@ let interp_casted_constr ocl ist sigma env (c,ce) = let interp_constr ist sigma env c = interp_casted_constr None ist sigma env c -(* Interprets an open constr expression casted by the current goal *) -let pf_interp_casted_openconstr ist gl (c,ce) = +(* Interprets an open constr expression *) +let pf_interp_openconstr ist gl (c,ce) = let sigma = project gl in let env = pf_env gl in let (ltacvars,l) = constr_list ist env in let typs = retype_list sigma env ltacvars in - let ocl = Some (pf_concl gl) in match ce with | None -> - Pretyping.understand_gen_tcc sigma env typs ocl c + Pretyping.understand_gen_tcc sigma env typs None c (* If at toplevel (ce<>None), the error can be due to an incorrect context at globalization time: we retype with the now known intros/lettac/inversion hypothesis names *) - | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl + | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c None (* Interprets a constr expression *) let pf_interp_constr ist gl = @@ -1586,9 +1585,9 @@ and interp_genarg ist goal x = | RedExprArgType -> in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x)) | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x) - | CastedOpenConstrArgType -> - in_gen wit_casted_open_constr - (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x)) + | OpenConstrArgType -> + in_gen wit_open_constr + (pf_interp_openconstr ist goal (snd (out_gen globwit_open_constr x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x)) @@ -1801,7 +1800,7 @@ and interp_atomic ist gl = function val_interp ist gl (out_gen globwit_tactic x) | StringArgType | BoolArgType | QuantHypArgType | RedExprArgType - | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ -> error "This generic type is not supported in alias" in @@ -2092,9 +2091,9 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) | TacticArgType -> in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x)) - | CastedOpenConstrArgType -> - in_gen globwit_casted_open_constr - (subst_rawconstr subst (out_gen globwit_casted_open_constr x)) + | OpenConstrArgType -> + in_gen globwit_open_constr + ((),subst_rawconstr subst (snd (out_gen globwit_open_constr x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x)) |