From c3e01a044297d322d8a5e6830fe3af002ebd2dce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Dec 2015 08:23:35 +0100
Subject: Fixing an "injection as" bug in the presence of side conditions.

---
 tactics/equality.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 92ebcb2724..1854b41205 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1319,13 +1319,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     tclZEROMSG (str "Failed to decompose the equality.")
   else
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
-    (Proofview.tclBIND
-      (Proofview.Monad.List.map
+    (Tacticals.New.tclTHENFIRST
+      (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
             Proofview.V82.tactic (refine pf)])
-         (if l2r then List.rev injectors else injectors))
-      (fun _ -> tac (List.length injectors)))
+         (if l2r then List.rev injectors else injectors)))
+      (tac (List.length injectors)))
 
 let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-- 
cgit v1.2.3