From d98fdf1ef5789f6d5420e52c34a33debf08584e9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Feb 2014 14:07:43 +0100
Subject: Code refactoring thanks to the new Monad module.

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

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 098e45a4aa..d6139f5297 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1196,7 +1196,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
   else
     Proofview.tclBIND
-      (Proofview.list_map
+      (Proofview.Monad.List.map
          (fun (pf,ty) -> Tacticals.New.tclTHENS (cut ty) [Proofview.tclUNIT (); Proofview.V82.tactic (refine pf)])
          (if l2r then List.rev injectors else injectors))
       (fun _ -> tac (List.length injectors))
-- 
cgit v1.2.3