Proofview.Notations: Now that (>>=) is free, use it for tclBIND.

Impacts MapleMode.

8 files changed, 58 insertions, 58 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74a1c56244..61e7dde181 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1117,7 +1117,7 @@ let conclPattern concl pat tac =
     | Some pat ->
 	try Proofview.tclUNIT (matches pat concl)
 	with PatternMatchingFailure -> Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) in
-    constr_bindings >= fun constr_bindings ->
+    constr_bindings >>= fun constr_bindings ->
     Hook.get forward_interp_tactic constr_bindings tac
 
 (***********************************************************)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index f5f09f27ec..81fab6e2bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -176,7 +176,7 @@ let double_ind h1 h2 =
     if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
     if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
       Proofview.tclZERO (Errors.UserError ("", Pp.str"Both hypotheses are the same.")) in
-  abs >= fun (abs_i,abs_j) ->
+  abs >>= fun (abs_i,abs_j) ->
   (Tacticals.New.tclTHEN (Tacticals.New.tclDO abs_i intro)
      (Tacticals.New.onLastHypId
        	(fun id ->
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index a98cb2a6f1..4b1cd87150 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -141,7 +141,7 @@ let solveEqBranch rectype =
     begin
       Proofview.Goal.enter begin fun gl ->
         let concl = Proofview.Goal.concl gl in
-        match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
+        match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
           let (mib,mip) = Global.lookup_inductive rectype in
           let nparams   = mib.mind_nparams in
           let getargs l = List.skipn nparams (snd (decompose_app l)) in
@@ -168,12 +168,12 @@ let decideGralEquality =
     begin
       Proofview.Goal.enter begin fun gl ->
         let concl = Proofview.Goal.concl gl in
-        match_eqdec concl >= fun (eqonleft,_,c1,c2,typ) ->
+        match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
         let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in
         begin match kind_of_term headtyp with
         | Ind mi -> Proofview.tclUNIT mi
         | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
-        end >= fun rectype ->
+        end >>= fun rectype ->
           (Tacticals.New.tclTHEN
              (mkBranches c1 c2)
              (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 033a4dc1b3..a397976ea9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -116,7 +116,7 @@ END
 
 open Proofview.Notations
 let discrHyp id =
-  Proofview.tclEVARMAP >= fun sigma ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   discr_main {it = Term.mkVar id,NoBindings; sigma = sigma;}
 
 let injection_main c =
@@ -161,7 +161,7 @@ TACTIC EXTEND einjection_as
 END
 
 let injHyp id =
-  Proofview.tclEVARMAP >= fun sigma ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
 
 TACTIC EXTEND dependent_rewrite
diff --git a/tactics/inv.ml b/tactics/inv.ml
index fb6de660d6..06853e137f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -426,7 +426,7 @@ let rewrite_equations othin neqns names ba =
 		 (Tacticals.New.onLastHypId (fun id ->
 		   Tacticals.New.tclTRY (projectAndApply thin id first_eq names depids)))))
 	       names;
-	     Tacticals.New.tclMAP (fun (id,_,_) -> Proofview.tclUNIT () >= fun () -> (* delay for [first_eq]. *)
+	     Tacticals.New.tclMAP (fun (id,_,_) -> Proofview.tclUNIT () >>= fun () -> (* delay for [first_eq]. *)
 	       intro_move None (if thin then MoveLast else !first_eq))
 	       nodepids;
 	     Proofview.V82.tactic (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)]
@@ -470,7 +470,7 @@ let raw_inversion inv_kind id status names =
       with UserError _ ->
         Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
 	                                     str ("The type of "^(Id.to_string id)^" is not inductive.")))
-    end >= fun (ind,t) ->
+    end >>= fun (ind,t) ->
     try
       let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in
       let ccl = clenv_type indclause in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 171c248584..3d0c65862f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1044,7 +1044,7 @@ and interp_ltac_reference loc' mustbetac ist r gl =
         try Id.Map.find id ist.lfun
         with Not_found -> in_gen (topwit wit_var) id
       in
-      force_vrec ist v gl >= fun v ->
+      force_vrec ist v gl >>= fun v ->
       let v = propagate_trace ist loc id v in
       if mustbetac then Proofview.tclUNIT (coerce_to_tactic loc id v) else Proofview.tclUNIT v
   | ArgArg (loc,r) ->
@@ -1058,7 +1058,7 @@ and interp_ltac_reference loc' mustbetac ist r gl =
 and interp_tacarg ist arg gl =
   match arg with
   | TacGeneric arg ->
-      Proofview.tclEVARMAP >= fun sigma ->
+      Proofview.tclEVARMAP >>= fun sigma ->
       Proofview.V82.wrap_exceptions begin fun () ->
         let goal = Proofview.Goal.goal gl in
         let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
@@ -1067,7 +1067,7 @@ and interp_tacarg ist arg gl =
       end
   | Reference r -> interp_ltac_reference dloc false ist r gl
   | ConstrMayEval c ->
-      Proofview.tclEVARMAP >= fun sigma ->
+      Proofview.tclEVARMAP >>= fun sigma ->
       Proofview.V82.wrap_exceptions begin fun () ->
         let env = Proofview.Goal.env gl in
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
@@ -1078,24 +1078,24 @@ and interp_tacarg ist arg gl =
   | TacCall (loc,r,[]) ->
       interp_ltac_reference loc true ist r gl
   | TacCall (loc,f,l) ->
-      interp_ltac_reference loc true ist f gl >= fun fv ->
+      interp_ltac_reference loc true ist f gl >>= fun fv ->
       List.fold_right begin fun a acc ->
-        interp_tacarg ist a gl >= fun a_interp ->
-        acc >= fun acc ->
+        interp_tacarg ist a gl >>= fun a_interp ->
+        acc >>= fun acc ->
         Proofview.tclUNIT (a_interp::acc)
-      end l (Proofview.tclUNIT []) >= fun largs ->
+      end l (Proofview.tclUNIT []) >>= fun largs ->
       interp_app loc ist fv largs gl
   | TacExternal (loc,com,req,la) ->
       List.fold_right begin fun a acc ->
-        interp_tacarg ist a gl >= fun a_interp ->
-        acc >= fun acc ->
+        interp_tacarg ist a gl >>= fun a_interp ->
+        acc >>= fun acc ->
         Proofview.tclUNIT (a_interp::acc)
-      end la (Proofview.tclUNIT []) >= fun la_interp ->
+      end la (Proofview.tclUNIT []) >>= fun la_interp ->
       Proofview.V82.wrap_exceptions begin fun () ->
         interp_external loc ist gl com req la_interp
       end
   | TacFreshId l ->
-      Proofview.Goal.refresh_sigma gl >= fun gl ->
+      Proofview.Goal.refresh_sigma gl >>= fun gl ->
       (* spiwack: I'm probably being over-conservative here,
          pf_interp_fresh_id shouldn't raise exceptions *)
       Proofview.V82.wrap_exceptions begin fun () ->
@@ -1149,7 +1149,7 @@ and interp_app loc ist fv largs gl =
               Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
 	      Proofview.tclZERO e
             end
-        end >= fun v ->
+        end >>= fun v ->
         (* No errors happened, we propagate the trace *)
         let v = append_trace trace v in
         let env = Proofview.Goal.env gl in
@@ -1183,7 +1183,7 @@ and tactic_of_value ist vle =
   else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
 
 and eval_value ist tac gl =
-  val_interp ist tac gl >= fun v ->
+  val_interp ist tac gl >>= fun v ->
   if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
   | VFun (trace,lfun,[],t) ->
       let ist = {
@@ -1196,7 +1196,7 @@ and eval_value ist tac gl =
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u gl =
-  Proofview.tclUNIT () >= fun () -> (* delay for the effects of [lref], just in case. *)
+  Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
   let fold accu ((_, id), b) =
     let v = of_tacvalue (VRec (lref, TacArg (dloc, b))) in
@@ -1210,11 +1210,11 @@ and interp_letrec ist llc u gl =
 (* Interprets the clauses of a LetIn *)
 and interp_letin ist llc u gl =
   let fold ((_, id), body) acc =
-    interp_tacarg ist body gl >= fun v ->
-    acc >= fun acc ->
+    interp_tacarg ist body gl >>= fun v ->
+    acc >>= fun acc ->
     Proofview.tclUNIT (Id.Map.add id v acc)
   in
-  List.fold_right fold llc (Proofview.tclUNIT ist.lfun) >= fun lfun ->
+  List.fold_right fold llc (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
   let ist = { ist with lfun } in
   val_interp ist u gl
 
@@ -1281,8 +1281,8 @@ and interp_match ist lz constr lmr gl =
           (fun () -> str "evaluation of the matched expression")) <*>
           Proofview.tclZERO e
     end
-  end >= fun constr ->
-  Proofview.tclEVARMAP >= fun sigma ->
+  end >>= fun constr ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
     let env = Proofview.Goal.env gl in
     let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
@@ -1291,7 +1291,7 @@ and interp_match ist lz constr lmr gl =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr gl =
-    Proofview.tclEVARMAP >= fun sigma ->
+    Proofview.tclEVARMAP >>= fun sigma ->
     Proofview.V82.wrap_exceptions begin fun () ->
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
@@ -1302,7 +1302,7 @@ and interp_match_goal ist lz lr lmr gl =
     end
 
 and interp_external loc ist gl com req la =
-  Proofview.Goal.refresh_sigma gl >= fun gl ->
+  Proofview.Goal.refresh_sigma gl >>= fun gl ->
   let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in
   let g ch = internalise_tacarg ch in
   interp_tacarg ist (System.connect f g com) gl
@@ -1407,7 +1407,7 @@ and interp_ltac_constr ist e gl =
             Proofview.tclZERO Not_found
         | e -> Proofview.tclZERO e
       end
-  end >= fun result ->
+  end >>= fun result ->
   Proofview.V82.wrap_exceptions begin fun () ->
   let env = Proofview.Goal.env gl in
   let result = Value.normalize result in
@@ -1438,7 +1438,7 @@ and interp_tactic ist tac =
     tactic_of_value ist (val_interp_glob ist tac)
   with NeedsAGoal ->
     Proofview.Goal.enter begin fun gl ->
-      val_interp ist tac gl >= fun v ->
+      val_interp ist tac gl >>= fun v ->
       tactic_of_value ist v
     end
 
@@ -1588,7 +1588,7 @@ and interp_atomic ist tac =
   | TacCut c ->
       let open Proofview.Notations in
       Proofview.Goal.enter begin fun gl ->
-        new_interp_type ist c gl >= Tactics.cut
+        new_interp_type ist c gl >>= Tactics.cut
       end
   | TacAssert (t,ipat,c) ->
       Proofview.Goal.enter begin fun gl ->
@@ -1967,7 +1967,7 @@ and interp_atomic ist tac =
       | ConstrWithBindingsArgType
       | BindingsArgType
       | OptArgType _ | PairArgType _ -> (** generic handler *)
-        Proofview.tclEVARMAP >= fun sigma ->
+        Proofview.tclEVARMAP >>= fun sigma ->
         Proofview.V82.wrap_exceptions begin fun () ->
           let env = Proofview.Goal.env gl in
           let concl = Proofview.Goal.concl gl in
@@ -1976,8 +1976,8 @@ and interp_atomic ist tac =
           Proofview.V82.tclEVARS sigma <*> Proofview.tclUNIT arg
         end
       | _ as tag -> (** Special treatment. TODO: use generic handler  *)
-        Proofview.tclEVARMAP >= fun sigma ->
-        Proofview.Goal.refresh_sigma gl >= fun gl ->
+        Proofview.tclEVARMAP >>= fun sigma ->
+        Proofview.Goal.refresh_sigma gl >>= fun gl ->
         Proofview.V82.wrap_exceptions begin fun () ->
           let env = Proofview.Goal.env gl in
         match tag with
@@ -2036,10 +2036,10 @@ and interp_atomic ist tac =
               (* spiwack: unsafe, we should introduce relevant combinators.
                  Before new tactical it simply read: [Genarg.app_list f x] *)
               fold_list begin fun a l ->
-                f a gl >= fun a' ->
-                l >= fun l ->
+                f a gl >>= fun a' ->
+                l >>= fun l ->
                 Proofview.tclUNIT (a'::l)
-              end x (Proofview.tclUNIT []) >= fun l ->
+              end x (Proofview.tclUNIT []) >>= fun l ->
 		let wit_t = Obj.magic t in
 		let l = List.map (fun arg -> out_gen wit_t arg) l in
               Proofview.tclUNIT (in_gen
@@ -2049,7 +2049,7 @@ and interp_atomic ist tac =
               (** Special treatment of tactics *)
               if has_type x (glbwit wit_tactic) then
                 let tac = out_gen (glbwit wit_tactic) x in
-                val_interp ist tac gl >= fun v ->
+                val_interp ist tac gl >>= fun v ->
                 Proofview.tclUNIT v
               else
                 let goal = Proofview.Goal.goal gl in
@@ -2061,11 +2061,11 @@ and interp_atomic ist tac =
       in
       Proofview.Goal.enter begin fun gl ->
         let addvar (x, v) accu =
-          accu >= fun accu ->
-          f v gl >= fun v ->
+          accu >>= fun accu ->
+          f v gl >>= fun v ->
           Proofview.tclUNIT (Id.Map.add x v accu)
         in
-        List.fold_right addvar l (Proofview.tclUNIT ist.lfun) >= fun lfun ->
+        List.fold_right addvar l (Proofview.tclUNIT ist.lfun) >>= fun lfun ->
           let trace = push_trace (loc,LtacNotationCall s) ist in
           let ist = {
             lfun = lfun;
@@ -2080,7 +2080,7 @@ let default_ist () =
   { lfun = Id.Map.empty; extra = extra }
 
 let eval_tactic t =
-  Proofview.tclUNIT () >= fun () -> (* delay for [default_ist] *)
+  Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
   Proofview.tclLIFT db_initialize <*>
   interp_tactic (default_ist ()) t
 
@@ -2120,7 +2120,7 @@ let hide_interp global t ot =
     | Some t' -> Tacticals.New.tclTHEN t t'
   in
   if global then
-    Proofview.tclENV >= fun env ->
+    Proofview.tclENV >>= fun env ->
     hide_interp env
   else
     Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 639c4c97bc..c6a3a0012d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -501,7 +501,7 @@ module New = struct
     tclREPEAT_MAIN0 (tclPROGRESS t)
 
   let tclCOMPLETE t =
-    t >= fun res ->
+    t >>= fun res ->
       (tclINDEPENDENT
          (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
       ) <*>
@@ -514,7 +514,7 @@ module New = struct
     Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
 
   let tclWITHHOLES accept_unresolved_holes tac sigma x =
-    tclEVARMAP >= fun sigma_initial ->
+    tclEVARMAP >>= fun sigma_initial ->
       if sigma == sigma_initial then tac x
       else
         let check_evars env new_sigma sigma initial_sigma =
@@ -526,8 +526,8 @@ module New = struct
         in
         let check_evars_if =
           if not accept_unresolved_holes then
-            tclEVARMAP >= fun sigma_final ->
-              tclENV >= fun env ->
+            tclEVARMAP >>= fun sigma_final ->
+              tclENV >>= fun env ->
                 check_evars env sigma_final sigma sigma_initial
           else
             tclUNIT ()
@@ -556,11 +556,11 @@ module New = struct
 
   let onNthHypId m tac =
     Goal.enter begin fun gl ->
-      Proofview.tclUNIT (nthHypId m gl) >= tac
+      Proofview.tclUNIT (nthHypId m gl) >>= tac
     end
   let onNthHyp m tac =
     Goal.enter begin fun gl ->
-      Proofview.tclUNIT (nthHyp m gl) >= tac
+      Proofview.tclUNIT (nthHyp m gl) >>= tac
     end
 
   let onLastHypId = onNthHypId 1
@@ -568,7 +568,7 @@ module New = struct
 
   let onNthDecl m tac =
     Proofview.Goal.enter begin fun gl ->
-      Proofview.tclUNIT (nthDecl m gl) >= tac
+      Proofview.tclUNIT (nthDecl m gl) >>= tac
     end
   let onLastDecl  = onNthDecl 1
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b4b6934f25..fe26bbb2db 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1983,7 +1983,7 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
 let make_eq_test c = (make_eq_test c,fun _ -> c)
 
 let letin_tac with_eq name c ty occs =
-  Proofview.tclEVARMAP >= fun sigma ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
 
 let letin_pat_tac with_eq name c ty occs =
@@ -3412,7 +3412,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
   Tacticals.New.tclTHENLIST
     [
       (atomize_list lc);
-      (Proofview.tclUNIT () >= fun () -> (* recompute each time to have the new value of newlc *)
+      (Proofview.tclUNIT () >>= fun () -> (* recompute each time to have the new value of newlc *)
 	induction_without_atomization isrec with_evars elim names !newlc) ;
       (* after induction, try to unfold all letins created by atomize_list
          FIXME: unfold_all does not exist anywhere else? *)
@@ -3688,7 +3688,7 @@ let symmetry_red allowred =
       let sigma = Proofview.Goal.sigma gl in
       whd_betadeltaiota env sigma c
   in
-  match_with_equation concl >= fun with_eqn ->
+  match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
       Proofview.V82.tactic begin
@@ -3718,7 +3718,7 @@ let symmetry_in id =
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin
-      match_with_equation t >= fun (_,hdcncl,eq) ->
+      match_with_equation t >>= fun (_,hdcncl,eq) ->
         let symccl = match eq with
           | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
           | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
@@ -3793,7 +3793,7 @@ let transitivity_red allowred t =
       let sigma = Proofview.Goal.sigma gl in
       whd_betadeltaiota env sigma c
   in
-  match_with_equation concl >= fun with_eqn ->
+  match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
       Proofview.V82.tactic begin
@@ -3885,7 +3885,7 @@ let tclABSTRACT name_op tac gl =
 
 
 let admit_as_an_axiom =
-  Proofview.tclUNIT () >= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
+  Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
   simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
   Proofview.mark_as_unsafe