diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a088070342..967d7d7b8b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1135,7 +1135,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | TacFail (n,s) -> let msg = interp_message ist s in - let tac l = Proofview.V82.tactic (fun gl -> tclFAIL (interp_int_or_var ist n) l gl) in + let tac l = Proofview.tclINDEPENDENT (Tacticals.New.tclFAIL (interp_int_or_var ist n) l) in Ftactic.run msg tac | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> |
