diff options
| author | Arnaud Spiwack | 2014-12-23 13:06:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-23 13:40:05 +0100 |
| commit | 2fce10d6e0b65f10ac2cd06bf34310b7fce62738 (patch) | |
| tree | 40223f1b8bdc41b9240289e5de2a5e712120345f /tactics | |
| parent | f1699f6dbfa6254041da9ef9d576da05b02ba865 (diff) | |
A global [gfail] tactic which works like [fail] except that it fails even if there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
3 files changed, 10 insertions, 5 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index dfb3def564..5351e41698 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -222,7 +222,7 @@ let initial_atomic () = let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in List.iter iter [ "idtac",TacId []; - "fail", TacFail(ArgArg 0,[]); + "fail", TacFail(TacLocal,ArgArg 0,[]); "fresh", TacArg(dloc,TacFreshId []) ] diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c0e18c1f28..b5731e3bd5 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -611,8 +611,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) - | TacFail (n,l) -> - ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l) + | TacFail (g,n,l) -> + ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l) | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac) | TacAbstract (tac,s) -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 967d7d7b8b..89f6fbc747 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1133,9 +1133,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run msgnl begin fun msgnl -> print msgnl <*> log msgnl <*> break end - | TacFail (n,s) -> + | TacFail (g,n,s) -> let msg = interp_message ist s in - let tac l = Proofview.tclINDEPENDENT (Tacticals.New.tclFAIL (interp_int_or_var ist n) l) in + let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in + let tac = + match g with + | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l) + | TacGlobal -> tac + in Ftactic.run msg tac | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> |