From 27d780bd52e1776afb05793d43ac030af861c82d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Feb 2014 12:54:29 +0100
Subject: Proofview.Notations: Now that (>>=) is free, use it for tclBIND.

Impacts MapleMode.
---
 proofs/proofview.ml  | 12 ++++++------
 proofs/proofview.mli |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d42ea8b804..0dbbdca7cb 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -641,7 +641,7 @@ let in_proofview p k =
 
 
 module Notations = struct
-  let (>=) = tclBIND
+  let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 end
@@ -650,8 +650,8 @@ open Notations
 let rec list_map f = function
   | [] -> tclUNIT []
   | a::l ->
-      f a >= fun a' ->
-      list_map f l >= fun l' ->
+      f a >>= fun a' ->
+      list_map f l >>= fun l' ->
       tclUNIT (a'::l')
 
 
@@ -807,8 +807,8 @@ module Goal = struct
   end
   let enter f =
     list_iter_goal () begin fun goal () ->
-      Proof.current >= fun env ->
-      tclEVARMAP >= fun sigma ->
+      Proof.current >>= fun env ->
+      tclEVARMAP >>= fun sigma ->
       try
         (* enter_t cannot modify the sigma. *)
         let (t,_) = Goal.eval (enter_t f) env sigma goal in
@@ -822,7 +822,7 @@ module Goal = struct
   (* compatibility *)
   let goal { self=self } = self
   let refresh_sigma g =
-    tclEVARMAP >= fun sigma ->
+    tclEVARMAP >>= fun sigma ->
     tclUNIT { g with sigma }
 
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index c608bc8414..60a6c558cf 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -270,7 +270,7 @@ val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
 module Notations : sig
 
   (* tclBIND *)
-  val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+  val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
   (* [t >>= k] is [t >= fun l -> tclDISPATCH (List.map k l)].
      The [t] is supposed to return a list of values of the size of the
      list of goals. [k] is then applied to each of this value in the
-- 
cgit v1.2.3