diff options
| author | Arnaud Spiwack | 2014-12-19 18:17:03 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-23 13:40:05 +0100 |
| commit | f1699f6dbfa6254041da9ef9d576da05b02ba865 (patch) | |
| tree | d2721d2fe0e6a0e50cf29f7be67f2de35fec057a | |
| parent | 239fe70ae8a39f5c5619cf88f1ae264c31bda65e (diff) | |
Remove compatibility layer from Ltac's [fail].
| -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 -> |