diff options
author | 2013-11-25 22:30:02 +0100 | |
---|---|---|
committer | 2013-11-30 17:00:34 +0100 | |
commit | a01a60b366307da3eca63c9937984db6f273dc41 (patch) | |
tree | c8a5f42e5db1fd763367390a49d0611a68e33bf5 | |
parent | b86e7c1247fa4b34b75cf20ef24a8e0b6ba6eff1 (diff) |
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.
-rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
-rw-r--r-- | grammar/q_coqast.ml4 | 2 | ||||
-rw-r--r-- | interp/constrarg.ml | 6 | ||||
-rw-r--r-- | interp/constrarg.mli | 4 | ||||
-rw-r--r-- | lib/genarg.ml | 6 | ||||
-rw-r--r-- | lib/genarg.mli | 2 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
-rw-r--r-- | parsing/pcoq.ml4 | 4 | ||||
-rw-r--r-- | parsing/pcoq.mli | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 6 | ||||
-rw-r--r-- | tactics/extraargs.ml4 | 2 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 21 | ||||
-rw-r--r-- | tactics/extratactics.mli | 2 | ||||
-rw-r--r-- | tactics/tacintern.ml | 6 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 15 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 6 |
16 files changed, 47 insertions, 43 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index d884a10cb..dc521e20d 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -39,7 +39,7 @@ let rec make_wit loc = function | ConstrArgType -> <:expr< Constrarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >> | RedExprArgType -> <:expr< Constrarg.wit_red_expr >> - | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Constrarg.wit_bindings >> | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 02c00e3f0..b405539ec 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -207,7 +207,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> + | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 16af7c308..97004a93d 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -60,11 +60,7 @@ let wit_constr = unsafe_of_type ConstrArgType let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType -let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b) - -let wit_open_constr = wit_open_constr_gen false - -let wit_casted_open_constr = wit_open_constr_gen true +let wit_open_constr = unsafe_of_type OpenConstrArgType let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 1233e165f..b83c20065 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -57,12 +57,8 @@ val wit_constr_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 wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type - val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type -val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type - val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, diff --git a/lib/genarg.ml b/lib/genarg.ml index 98287d184..0f1e50568 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -20,7 +20,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType @@ -38,7 +38,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | ConstrArgType, ConstrArgType -> true | ConstrMayEvalArgType, ConstrMayEvalArgType -> true | QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 +| OpenConstrArgType, OpenConstrArgType -> true | ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true | BindingsArgType, BindingsArgType -> true | RedExprArgType, RedExprArgType -> true @@ -59,7 +59,7 @@ let rec pr_argument_type = function | ConstrArgType -> str "constr" | ConstrMayEvalArgType -> str "constr_may_eval" | QuantHypArgType -> str "qhyp" -| OpenConstrArgType _ -> str "open_constr" +| OpenConstrArgType -> str "open_constr" | ConstrWithBindingsArgType -> str "constr_with_bindings" | BindingsArgType -> str "bindings" | RedExprArgType -> str "redexp" diff --git a/lib/genarg.mli b/lib/genarg.mli index e2654fcf5..3d5828bbb 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -199,7 +199,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index eb483c50c..93afb3d5a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -215,7 +215,7 @@ let merge_occurrences loc cl = function GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var open_constr casted_open_constr + bindings red_expr int_or_var open_constr simple_intropattern; int_or_var: @@ -236,9 +236,6 @@ GEXTEND Gram open_constr: [ [ c = constr -> ((),c) ] ] ; - casted_open_constr: - [ [ c = constr -> ((),c) ] ] - ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n | c = constr_with_bindings -> induction_arg_of_constr c diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 79228e946..d25efa72a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -377,9 +377,7 @@ 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 (wit_open_constr_gen false)) "open_constr" - let casted_open_constr = - make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr" + make_gen_entry utactic (rawwit wit_open_constr) "open_constr" let constr_with_bindings = make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" let bindings = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index bbb71a170..56282f2f6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,7 +213,6 @@ module Tactic : sig open Glob_term val open_constr : open_constr_expr Gram.entry - val casted_open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e1324c3ee..f091a2e1d 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -158,7 +158,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi | RedExprArgType -> pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) (out_gen (rawwit wit_red_expr) x) - | OpenConstrArgType b -> prc (snd (out_gen (rawwit (wit_open_constr_gen b)) x)) + | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) | BindingsArgType -> @@ -196,7 +196,7 @@ let rec pr_glb_generic prc prlc prtac prpat x = pr_red_expr (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) (out_gen (glbwit wit_red_expr) x) - | OpenConstrArgType b -> prc (snd (out_gen (glbwit (wit_open_constr_gen b)) x)) + | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) | BindingsArgType -> @@ -227,7 +227,7 @@ let rec pr_top_generic prc prlc prtac prpat x = | RedExprArgType -> pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) (out_gen (topwit wit_red_expr) x) - | OpenConstrArgType b -> prc (snd (out_gen (topwit (wit_open_constr_gen b)) x)) + | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) | ConstrWithBindingsArgType -> let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in pr_with_bindings prc prlc (c,b) diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index ccc231cf2..a3c531f80 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 c81e7ce3f..18326435c 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 7a0fabe1f..2b28a6547 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 261e8583e..19ab65d22 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 0821423b5..ce216b15d 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 7491c9a8f..57aa88368 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)) |