From f1699f6dbfa6254041da9ef9d576da05b02ba865 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 19 Dec 2014 18:17:03 +0100
Subject: Remove compatibility layer from Ltac's [fail].

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 ->
-- 
cgit v1.2.3