diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 17:34:03 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 19:06:22 +0200 |
commit | e8d79faee901881fc08ea31761d530832105eaf7 (patch) | |
tree | 7cd611e4efb86605f577f6a98932dc14307959ba /tactics | |
parent | fc4fa4e42289cd13a8732ff2e08bf33ba1708928 (diff) |
A slightly more fine grained way to check whether a TACTIC EXTEND is global or local to goals.
Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tacinterp.ml | 30 |
1 files changed, 25 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3bccbf41f..601176ff6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1376,6 +1376,19 @@ and interp_genarg ist env sigma concl gl x = let v = interp_genarg x in !evdref , v + +(** returns [true] for genargs which have the same meaning + independently of goals. *) + +and global_genarg = + let rec global_tag = function + | IntOrVarArgType | GenArgType -> true + | ListArgType t | OptArgType t -> global_tag t + | PairArgType (t1,t2) -> global_tag t1 && global_tag t2 + | _ -> false + in + fun x -> global_tag (genarg_tag x) + and interp_genarg_constr_list ist env sigma x = let lc = out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in @@ -1798,12 +1811,19 @@ and interp_atomic ist tac : unit Proofview.tactic = end (* For extensions *) - | TacExtend (loc,opn,[]) -> - (* spiwack: a special case for tactics (from TACTIC EXTEND) without arguments to - be interpreted without a [Proofview.Goal.enter]. Eventually we should make - something more fine-grained by modifying [interp_genarg]. *) + | TacExtend (loc,opn,l) when List.for_all global_genarg l -> + (* spiwack: a special case for tactics (from TACTIC EXTEND) when + every argument can be interpreted without a + [Proofview.Goal.enter]. *) let tac = Tacenv.interp_ml_tactic opn in - tac [] ist + (* dummy values, will be ignored *) + let env = Environ.empty_env in + let sigma = Evd.empty in + let concl = Term.mkRel (-1) in + let goal = sig_it Goal.V82.dummy_goal in + (* /dummy values *) + let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in + tac args ist | TacExtend (loc,opn,l) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in |