From a01a60b366307da3eca63c9937984db6f273dc41 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 25 Nov 2013 22:30:02 +0100 Subject: Getting rid of casted_open_constr. It was only used by the refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK. --- tactics/extraargs.ml4 | 2 +- tactics/extratactics.ml4 | 21 ++++++++++++++++++++- tactics/extratactics.mli | 2 +- tactics/tacintern.ml | 6 +++--- tactics/tacinterp.ml | 15 +++++++-------- tactics/tacsubst.ml | 6 +++--- 6 files changed, 35 insertions(+), 17 deletions(-) (limited to 'tactics') diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index ccc231cf2d..a3c531f80a 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -116,7 +116,7 @@ ARGUMENT EXTEND glob GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen - [ lconstr(c) ] -> [ c ] + [ constr(c) ] -> [ c ] END diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c81e7ce3f1..18326435c6 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -324,8 +324,27 @@ END let refine_tac = Tactics.New.refine +let refine_red_flags = + Genredexpr.Lazy { + Genredexpr.rBeta=true; + rIota=true; + rZeta=false; + rDelta=false; + rConst=[]; + } + +let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences } + +let refine_tac (ist, c) = + let c = Goal.Refinable.make begin fun h -> + Goal.Refinable.constr_of_raw h true true c + end in + Proofview.Goal.lift c >>= fun c -> + Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.V82.tactic (reduce refine_red_flags refine_locs) + TACTIC EXTEND refine - [ "refine" casted_open_constr(c) ] -> [ refine_tac c ] + [ "refine" glob(c) ] -> [ refine_tac c ] END (**********************************************************************) diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 7a0fabe1fa..2b28a65471 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -11,6 +11,6 @@ open Proof_type val discrHyp : Names.Id.t -> unit Proofview.tactic val injHyp : Names.Id.t -> unit Proofview.tactic -val refine_tac : Evd.open_constr -> unit Proofview.tactic +(* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 261e8583e1..19ab65d224 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -736,9 +736,9 @@ and intern_genarg ist x = (intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x)) | RedExprArgType -> in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x)) - | OpenConstrArgType b -> - in_gen (glbwit (wit_open_constr_gen b)) - ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x))) + | OpenConstrArgType -> + in_gen (glbwit wit_open_constr) + ((),intern_constr ist (snd (out_gen (rawwit wit_open_constr) x))) | ConstrWithBindingsArgType -> in_gen (glbwit wit_constr_with_bindings) (intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x)) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0821423b5d..ce216b15d1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -144,7 +144,7 @@ let pr_inspect env expr result = let pp_result = if has_type result (topwit wit_tacvalue) then match to_tacvalue result with - | VRTactic _ -> str "a VRTactic" + | VRTactic -> str "a VRTactic" | VFun (_, il, ul, b) -> let pp_body = Pptactic.pr_glob_tactic env b in let pr_sep () = str ", " in @@ -1346,13 +1346,12 @@ and interp_genarg ist env sigma concl gl x = in evdref := sigma; in_gen (topwit wit_red_expr) r_interp - | OpenConstrArgType casted -> - let expected_type = - if casted then OfType concl else WithoutTypeConstraint in - in_gen (topwit (wit_open_constr_gen casted)) + | OpenConstrArgType -> + let expected_type = WithoutTypeConstraint in + in_gen (topwit wit_open_constr) (interp_open_constr ~expected_type ist env !evdref - (snd (out_gen (glbwit (wit_open_constr_gen casted)) x))) + (snd (out_gen (glbwit wit_open_constr) x))) | ConstrWithBindingsArgType -> in_gen (topwit wit_constr_with_bindings) (pack_sigma (interp_constr_with_bindings ist env !evdref @@ -1983,7 +1982,7 @@ and interp_atomic ist tac = Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) -> (Proofview.V82.tclEVARS sigma) <*> (Proofview.Goal.return v) - | OpenConstrArgType false -> + | OpenConstrArgType -> Proofview.Goal.return ( Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) -> (Proofview.V82.tclEVARS sigma) <*> @@ -2043,7 +2042,7 @@ and interp_atomic ist tac = Proofview.V82.tactic (tclEVARS newsigma) <*> Proofview.Goal.return v | QuantHypArgType | RedExprArgType - | OpenConstrArgType _ | ConstrWithBindingsArgType + | ConstrWithBindingsArgType | BindingsArgType | OptArgType _ | PairArgType _ -> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations.")) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 7491c9a8f8..57aa883687 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -312,9 +312,9 @@ and subst_genarg subst (x:glob_generic_argument) = (out_gen (glbwit wit_quant_hyp) x)) | RedExprArgType -> in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x)) - | OpenConstrArgType b -> - in_gen (glbwit (wit_open_constr_gen b)) - ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x))) + | OpenConstrArgType -> + in_gen (glbwit wit_open_constr) + ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x))) | ConstrWithBindingsArgType -> in_gen (glbwit wit_constr_with_bindings) (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x)) -- cgit v1.2.3