Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 243 insertions, 243 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8115376c98..fd6dd03613 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1277,12 +1277,12 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   let intro_tac =
     Tacticals.New.tclTHEN (dbg_intro dbg)
       ( Proofview.tclEVARMAP >= fun sigma ->
-        Proofview.Goal.env >>- fun env ->
-        Tacmach.New.pf_last_hyp >>- fun hyp ->
+        Proofview.Goal.env >>= fun env ->
+        Tacmach.New.pf_last_hyp >>= fun hyp ->
 	let hintl = make_resolve_hyp env sigma hyp
 	in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db))
   in
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>= fun concl ->
   Tacticals.New.tclFIRST
     ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
      (List.map Tacticals.New.tclCOMPLETE
@@ -1375,7 +1375,7 @@ let make_db_list dbnames =
 let trivial ?(debug=Off) lems dbnames =
   let db_list = make_db_list dbnames in
   let d = mk_trivial_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>- fun hints ->
+  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
   new_tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
 
@@ -1384,7 +1384,7 @@ let full_trivial ?(debug=Off) lems =
   let dbs = String.Map.remove "v62" dbs in
   let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_trivial_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>- fun hints ->
+  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
   new_tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
 
@@ -1420,7 +1420,7 @@ let extend_local_db gl decl db =
 
 let intro_register dbg kont db =
   Tacticals.New.tclTHEN (dbg_intro dbg)
-    (Tacmach.New.of_old extend_local_db >>- fun extend_local_db ->
+    (Tacmach.New.of_old extend_local_db >>= fun extend_local_db ->
       Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)))
 
 (* n is the max depth of search *)
@@ -1434,7 +1434,7 @@ let search d n mod_delta db_list local_db =
       if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
         Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
-	     ( Proofview.Goal.concl >>- fun concl ->
+	     ( Proofview.Goal.concl >>= fun concl ->
 	       let d' = incr_dbg d in
 	       Tacticals.New.tclFIRST
 	         (List.map
@@ -1450,7 +1450,7 @@ let delta_auto ?(debug=Off) mod_delta n lems dbnames =
   Proofview.tclUNIT () >= fun () -> (* delay for the side effects *)
   let db_list = make_db_list dbnames in
   let d = mk_auto_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>- fun hints ->
+  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
   new_tclTRY_dbg d
     (search d n mod_delta db_list hints)
 
@@ -1465,7 +1465,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems =
   let dbs = String.Map.remove "v62" dbs in
   let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_auto_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>- fun hints ->
+  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
   new_tclTRY_dbg d
     (search d n mod_delta db_list hints)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8a09ff7896..9c1f462bac 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -114,7 +114,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
  (* let's check at once if id exists (to raise the appropriate error) *)
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive idl) >>- fun _ ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive idl) >>= fun _ ->
  let general_rewrite_in id =
   let id = ref id in
   let to_be_cleared = ref false in
@@ -179,7 +179,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 	   | None ->
 		 (* try to rewrite in all hypothesis
 		    (except maybe the rewritten one) *)
-                 Tacmach.New.pf_ids_of_hyps >>- fun ids ->
+                 Tacmach.New.pf_ids_of_hyps >>= fun ids ->
 		 try_do_hyps (fun id -> id)  ids)
 
 let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT())
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f1ebdc6384..0725825e98 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,9 +83,9 @@ let rec eq_constr_mod_evars x y =
   | _, _ -> compare_constr eq_constr_mod_evars x y
 
 let progress_evars t =
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>= fun concl ->
   let check =
-      Proofview.Goal.concl >>- fun newconcl ->
+      Proofview.Goal.concl >>= fun newconcl ->
       if eq_constr_mod_evars concl newconcl
       then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
       else Proofview.tclUNIT ()
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index ed1661910e..7904c88eec 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -44,12 +44,12 @@ let filter_hyp f tac =
     | [] -> raise Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
-  Proofview.Goal.hyps >>- fun hyps ->
+  Proofview.Goal.hyps >>= fun hyps ->
   seek (Environ.named_context_of_val hyps)
 
 let contradiction_context =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   let rec seek_neg l = match l with
     | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
     | (id,_,typ)::rest ->
@@ -60,7 +60,7 @@ let contradiction_context =
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
                  begin
-                   Tacmach.New.pf_apply is_conv_leq >>- fun is_conv_leq ->
+                   Tacmach.New.pf_apply is_conv_leq >>= fun is_conv_leq ->
 	           filter_hyp (fun typ -> is_conv_leq typ t)
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                  end
@@ -69,7 +69,7 @@ let contradiction_context =
                    | e -> Proofview.tclZERO e
                  end)
 	  | _ -> seek_neg rest in
-  Proofview.Goal.hyps >>- fun hyps ->
+  Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
   seek_neg hyps
 
@@ -80,8 +80,8 @@ let is_negation_of env sigma typ t =
 
 let contradiction_term (c,lbind as cl) =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Proofview.Goal.env >>= fun env ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   let typ = type_of c in
   let _, ccl = splay_prod env sigma typ in
   if is_empty_type ccl then
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a784264f05..f8f85ef3c6 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -86,7 +86,7 @@ let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   let typc = type_of c in
   Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
     [ Tacticals.New.tclTHEN (intro_using tmphyp_name)
@@ -111,7 +111,7 @@ let head_in =
 
 let decompose_these c l =
   let indl = (*List.map inductive_of*) l in
-  Proofview.Goal.lift head_in >>- fun head_in ->
+  Proofview.Goal.lift head_in >>= fun head_in ->
   general_decompose (fun (_,t) -> head_in indl t) c
 
 let decompose_nonrec c =
@@ -167,8 +167,8 @@ let induction_trailer abs_i abs_j bargs =
           ))
 
 let double_ind h1 h2 =
-  Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) >>- fun abs_i ->
-  Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) >>- fun abs_j ->
+  Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) >>= fun abs_i ->
+  Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) >>= fun abs_j ->
   let abs =
     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
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index cc6547bc33..0a6e7a0724 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -120,8 +120,8 @@ let match_eqdec c =
 (* /spiwack *)
 
 let solveArg eqonleft op a1 a2 tac =
-  Tacmach.New.of_old (fun g -> pf_type_of g a1) >>- fun rectype ->
-  Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) >>- fun decide ->
+  Tacmach.New.of_old (fun g -> pf_type_of g a1) >>= fun rectype ->
+  Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) >>= fun decide ->
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
     else [diseqCase eqonleft;eqCase tac;default_auto] in
@@ -130,7 +130,7 @@ let solveArg eqonleft op a1 a2 tac =
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>- fun concl ->
+      Proofview.Goal.concl >>= fun concl ->
       match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
       let (mib,mip) = Global.lookup_inductive rectype in
       let nparams   = mib.mind_nparams in
@@ -155,9 +155,9 @@ let hd_app c = match kind_of_term c with
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>- fun concl ->
+      Proofview.Goal.concl >>= fun concl ->
       match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
-      Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>- fun headtyp ->
+      Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
       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."))
@@ -175,15 +175,15 @@ let decideGralEquality =
 let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality
 
 let decideEquality rectype =
-  Tacmach.New.of_old (mkGenDecideEqGoal rectype) >>- fun decide ->
+  Tacmach.New.of_old (mkGenDecideEqGoal rectype) >>= fun decide ->
   (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide)) [default_auto;decideEqualityGoal])
 
 
 (* The tactic Compare *)
 
 let compare c1 c2 =
-  Tacmach.New.of_old (fun g -> pf_type_of g c1) >>- fun rectype ->
-  Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) >>- fun decide ->
+  Tacmach.New.of_old (fun g -> pf_type_of g c1) >>= fun rectype ->
+  Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) >>= fun decide ->
   (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide))
             [(Tacticals.New.tclTHEN  intro
              (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ad306aba7..a7b04bee24 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -240,7 +240,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
          (Proofview.V82.tactic (general_elim_clause with_evars frzevars cls c elim)))
       tac
   in
-    Proofview.Goal.lift cs >>- fun cs ->
+    Proofview.Goal.lift cs >>= fun cs ->
     if firstonly then
       Tacticals.New.tclFIRST (List.map try_clause cs)
     else
@@ -330,9 +330,9 @@ let type_of_clause = function
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
-  type_of_clause cls >>- fun type_of_cls ->
+  type_of_clause cls >>= fun type_of_cls ->
   let dep = dep_proof_ok && dep_fun c type_of_cls in
-  Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) >>- fun (elim,effs) ->
+  Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) >>= fun (elim,effs) ->
   Proofview.V82.tactic (Tactics.emit_side_effects effs) <*>
   general_elim_clause with_evars frzevars tac cls c t l
     (match lft2rgt with None -> false | Some b -> b)
@@ -360,7 +360,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
     Proofview.tclEVARMAP >= fun sigma ->
-    Proofview.Goal.env >>- fun env ->
+    Proofview.Goal.env >>= fun env ->
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
@@ -452,7 +452,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
               Tacmach.New.pf_ids_of_hyps_sensitive >- fun ids_of_hyps ->
 	      Goal.return (Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps)
 	  in
-          Proofview.Goal.lift ids >>- fun ids ->
+          Proofview.Goal.lift ids >>= fun ids ->
           do_hyps_atleastonce ids
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
@@ -466,7 +466,7 @@ type delayed_open_constr_with_bindings =
 let general_multi_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.tclEVARMAP >= fun sigma ->
-    Proofview.Goal.env >>- fun env ->
+    Proofview.Goal.env >>= fun env ->
     let sigma,c = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars
       (general_multi_rewrite l2r with_evars ?tac c) sigma cl in
@@ -501,10 +501,10 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
       | None -> Proofview.tclUNIT ()
       | Some tac ->  Tacticals.New.tclCOMPLETE tac
   in
-  Tacmach.New.pf_apply get_type_of >>- fun get_type_of ->
+  Tacmach.New.pf_apply get_type_of >>= fun get_type_of ->
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
-  Tacmach.New.pf_apply is_conv >>- fun is_conv ->
+  Tacmach.New.pf_apply is_conv >>= fun is_conv ->
   if unsafe || (is_conv t1 t2) then
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
@@ -787,7 +787,7 @@ let rec build_discriminator sigma env dirn c sort = function
 *)
 
 let gen_absurdity id =
-  Tacmach.New.pf_get_hyp_typ id >>- fun hyp_typ ->
+  Tacmach.New.pf_get_hyp_typ id >>= fun hyp_typ ->
   if is_empty_type hyp_typ
   then
     simplest_elim (mkVar id)
@@ -846,26 +846,26 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.concl >>= fun concl ->
   match find_positions env sigma t1 t2 with
     | Inr _ ->
 	Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
     | Inl (cpath, (_,dirn), _) ->
-        Tacmach.New.pf_apply get_type_of >>- fun get_type_of ->
+        Tacmach.New.pf_apply get_type_of >>= fun get_type_of ->
 	let sort = get_type_of concl in
 	discr_positions env sigma u eq_clause cpath dirn sort
 
 let onEquality with_evars tac (c,lbindc) =
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
-  Tacmach.New.of_old make_clenv_binding >>- fun make_clenv_binding ->
+  Tacmach.New.of_old make_clenv_binding >>= fun make_clenv_binding ->
   let eq_clause = make_clenv_binding (c,t') lbindc in
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  Tacmach.New.of_old find_this_eq_data_decompose >>- fun find_this_eq_data_decompose ->
+  Tacmach.New.of_old find_this_eq_data_decompose >>= fun find_this_eq_data_decompose ->
   let eq,eq_args = find_this_eq_data_decompose eqn in
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
@@ -873,8 +873,8 @@ let onEquality with_evars tac (c,lbindc) =
 
 let onNegatedEquality with_evars tac =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.concl >>- fun ccl ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.concl >>= fun ccl ->
+  Proofview.Goal.env >>= fun env ->
   match kind_of_term (hnf_constr env sigma ccl) with
   | Prod (_,t,u) when is_empty_type u ->
       Tacticals.New.tclTHEN introf
@@ -1263,9 +1263,9 @@ let injConcl = injClause None false None
 let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>- fun sort ->
+  Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
     let sigma =  clause.evd in
-    Proofview.Goal.env >>- fun env ->
+    Proofview.Goal.env >>= fun env ->
       match find_positions env sigma t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn sort
@@ -1509,9 +1509,9 @@ let is_eq_x gl x (id,_,c) =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.hyps >>- fun hyps ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.hyps >>= fun hyps ->
+  Proofview.Goal.concl >>= fun concl ->
   let hyps = Environ.named_context_of_val hyps in
   (* The set of hypotheses using x *)
   let depdecls =
@@ -1554,9 +1554,9 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
    au bon endroit. Il faut convertir test en une Proofview.tactic
    pour la gestion des exceptions. *)
 let subst_one_var dep_proof_ok x =
-  Proofview.Goal.hyps >>- fun hyps ->
+  Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
-  Tacmach.New.pf_get_hyp x >>- fun (_,xval,_) ->
+  Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
   (* If x has a body, simply replace x with body and clear x *)
   if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else
   (* x is a variable: *)
@@ -1570,7 +1570,7 @@ let subst_one_var dep_proof_ok x =
         (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	 str".")
     with FoundHyp res -> res in
-  Tacmach.New.of_old found >>- fun (hyp,rhs,dir) ->
+  Tacmach.New.of_old found >>= fun (hyp,rhs,dir) ->
   subst_one dep_proof_ok x (hyp,rhs,dir)
 
 let subst_gen dep_proof_ok ids =
@@ -1595,7 +1595,7 @@ let default_subst_tactic_flags () =
 
 (* arnaud: encore des erreurs potentiels avec ces try/with *)
 let subst_all ?(flags=default_subst_tactic_flags ()) =
-  Tacmach.New.of_old find_eq_data_decompose >>- fun find_eq_data_decompose ->
+  Tacmach.New.of_old find_eq_data_decompose >>= fun find_eq_data_decompose ->
   let test (_,c) =
     try
       let lbeq,(_,x,y) = find_eq_data_decompose c in
@@ -1607,7 +1607,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) =
     with PatternMatchingFailure -> failwith "caught"
   in
   let test p = try Some (test p) with Failure _ -> None in
-  Tacmach.New.pf_hyps_types >>- fun hyps ->
+  Tacmach.New.pf_hyps_types >>= fun hyps ->
   let ids = List.map_filter test hyps in
   let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids
@@ -1646,12 +1646,12 @@ let rewrite_multi_assumption_cond cond_eq_term cl =
     | (id,_,t) ::rest ->
 	begin
 	  try
-            cond_eq_term t >>- fun dir ->
+            cond_eq_term t >>= fun dir ->
 	    general_multi_rewrite dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest
 	end
   in
-  Proofview.Goal.hyps >>- fun hyps ->
+  Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
   arec hyps
 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 80b06b2fb3..0555564bd1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -54,7 +54,7 @@ open Proofview.Notations
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   let sigma',evar = Evarutil.new_evar sigma env ~src typ in
   Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
     (Tactics.letin_tac None name evar None Locusops.nowhere)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 71b2bdfb6c..a37880170a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -646,7 +646,7 @@ END
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
-  Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+  Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
       Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
     hyps
@@ -663,12 +663,12 @@ let refl_equal =
   should be replaced by a call to the tactic but I don't know how to
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
-      Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>- fun type_of_a ->
+      Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>= fun type_of_a ->
        Tacticals.New.tclTHENLIST
          [Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
           begin
-            Proofview.Goal.concl >>- fun concl ->
-            Proofview.Goal.env >>- fun env ->
+            Proofview.Goal.concl >>= fun concl ->
+            Proofview.Goal.env >>= fun env ->
             Proofview.V82.tactic begin
 	      change_in_concl None
 	        (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)
@@ -681,15 +681,15 @@ let case_eq_intros_rewrite x =
   Proofview.Goal.lift begin
     Goal.concl >- fun concl ->
     Goal.return (nb_prod concl)
-  end >>- fun n ->
+  end >>= fun n ->
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
     begin
-      Proofview.Goal.concl >>- fun concl ->
-      Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+      Proofview.Goal.concl >>= fun concl ->
+      Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
       let n' = nb_prod concl in
-      Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>- fun h ->
+      Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h ->
       Tacticals.New.tclTHENLIST [
                     Tacticals.New.tclDO (n'-n-1) intro;
 		    Proofview.V82.tactic (Tacmach.introduction h);
@@ -715,13 +715,13 @@ let destauto t =
   with Found tac -> tac
 
 let destauto_in id = 
-  Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) >>- fun ctype ->
+  Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) >>= fun ctype ->
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.concl >>- fun concl -> destauto concl ]
+| [ "destauto" ] -> [ Proofview.Goal.concl >>= fun concl -> destauto concl ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 644f527a00..8e551d3f38 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -274,7 +274,7 @@ Nota: with Inversion_clear, only four useless hypotheses
 *)
 
 let generalizeRewriteIntros tac depids id =
-  Tacmach.New.of_old (dependent_hyps id depids) >>- fun dids ->
+  Tacmach.New.of_old (dependent_hyps id depids) >>= fun dids ->
   (Tacticals.New.tclTHENLIST
     [Proofview.V82.tactic (bring_hyps dids); tac;
      (* may actually fail to replace if dependent in a previous eq *)
@@ -302,7 +302,7 @@ let projectAndApply thin id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) >>- fun (t,t1,t2) ->
+    Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) >>= fun (t,t1,t2) ->
     match (kind_of_term t1, kind_of_term t2) with
     | Var id1, _ -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp true id)) depids id1
     | _, Var id2 -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp false id)) depids id2
@@ -331,7 +331,7 @@ let projectAndApply thin id eqname names depids =
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
 let rewrite_equations_gene othin neqns ba =
-  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>- fun (depids,nodepids) ->
+  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>= fun (depids,nodepids) ->
   let rewrite_eqns =
     match othin with
       | Some thin ->
@@ -398,7 +398,7 @@ let extract_eqn_names = function
 
 let rewrite_equations othin neqns names ba =
   let names = List.map (get_names true) names in
-  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>- fun (depids,nodepids) ->
+  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>= fun (depids,nodepids) ->
   let rewrite_eqns =
     let first_eq = ref MoveLast in
     match othin with
@@ -444,18 +444,18 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
 
 let raw_inversion inv_kind id status names =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.concl >>= fun concl ->
   let c = mkVar id in
-  Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>- fun reduce_to_atomic_ind ->
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   let (ind,t) =
     try
       reduce_to_atomic_ind (type_of c)
     with UserError _ ->
       errorlabstrm "raw_inversion"
 	(str ("The type of "^(Id.to_string id)^" is not inductive.")) in
-  Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>- fun indclause ->
+  Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
   let IndType (indf,realargs) = find_rectype env sigma ccl in
@@ -522,11 +522,11 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
  * back to their places in the hyp-list. *)
 
 let invIn k names ids id =
-  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>- fun hyps ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+  Proofview.Goal.concl >>= fun concl ->
   let nb_prod_init = nb_prod concl in
   let intros_replace_ids =
-    Proofview.Goal.concl >>- fun concl ->
+    Proofview.Goal.concl >>= fun concl ->
     let nb_of_new_hyp =
       nb_prod concl - (List.length hyps + nb_prod_init)
     in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 786f927369..06b067fcf4 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -284,9 +284,9 @@ let lemInv id c gls =
 let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
 
 let lemInvIn id c ids =
-  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>- fun hyps ->
+  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
   let intros_replace_ids =
-    Proofview.Goal.concl >>- fun concl ->
+    Proofview.Goal.concl >>= fun concl ->
     let nb_of_new_hyp  = nb_prod concl - List.length ids in
     if nb_of_new_hyp < 1  then
       intros_replacing ids
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 61db456dd7..d0ef1ec2e6 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -315,7 +315,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) : unit Proofview.tactic =
 
     (* let in without holes in the body => possibly dependent intro *)
     | LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
-        Proofview.Goal.concl >>- fun c ->
+        Proofview.Goal.concl >>= fun c ->
 	let newc = mkNamedLetIn id c1 t1 c in
 	Tacticals.New.tclTHEN
 	  (Proofview.V82.tactic (change_in_concl None newc))
@@ -383,7 +383,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) : unit Proofview.tactic =
 
 let refine (evd,c) =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals env evd in
   let c = Evarutil.nf_evar evd c in
   let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index fb9ca25079..30fe8d4aef 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1326,7 +1326,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
 			++ fnl () ++ Himsg.explain_typeclass_error env e)))
-  in Proofview.Notations.(>>-) (Proofview.Goal.lift info) (fun i -> treat i)
+  in Proofview.Notations.(>>=) (Proofview.Goal.lift info) (fun i -> treat i)
   
 let newtactic_init_setoid () = 
   try init_setoid (); Proofview.tclUNIT ()
@@ -1766,8 +1766,8 @@ let not_declared env ty rel =
 
 let setoid_proof ty fn fallback =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.concl >>= fun concl ->
   Proofview.tclORELSE
     begin
       try
@@ -1800,7 +1800,7 @@ let setoid_proof ty fn fallback =
 let setoid_reflexivity =
   setoid_proof "reflexive"
     (fun env evm car rel -> Proofview.V82.tactic (apply (get_reflexive_proof env evm car rel)))
-      (reflexivity_red true)
+    (reflexivity_red true)
 
 let setoid_symmetry =
   setoid_proof "symmetric"
@@ -1819,18 +1819,18 @@ let setoid_transitivity c =
     (transitivity_red true c)
 
 let setoid_symmetry_in id =
-  Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) >>- fun ctype ->
-    let binders,concl = decompose_prod_assum ctype in
-    let (equiv, args) = decompose_app concl in
-    let rec split_last_two = function
-      | [c1;c2] -> [],(c1, c2)
-      | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
-      | _ -> error "The term provided is not an equivalence."
-    in
-    let others,(c1,c2) = split_last_two args in
-    let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
-    let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
-    let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
+  Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) >>= fun ctype ->
+  let binders,concl = decompose_prod_assum ctype in
+  let (equiv, args) = decompose_app concl in
+  let rec split_last_two = function
+    | [c1;c2] -> [],(c1, c2)
+    | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
+    | _ -> error "The term provided is not an equivalence."
+  in
+  let others,(c1,c2) = split_last_two args in
+  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
+  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
+  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
     Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp))
       [ Proofview.V82.tactic (intro_replacing id);
 	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic (Tactics.assumption) ] ]
@@ -1840,6 +1840,7 @@ let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
 let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
 let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
 
+
 let implify id gl =
   let (_, b, ctype) = pf_get_hyp gl id in
   let binders,concl = decompose_prod_assum ctype in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d788ade4d0..1c5903d51c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1161,7 +1161,7 @@ and interp_ltac_reference loc' mustbetac ist = function
 
 and interp_tacarg ist arg =
   let tac_of_old f =
-    Tacmach.New.of_old f >>-- fun (sigma,v) ->
+    Tacmach.New.of_old f >>== fun (sigma,v) ->
     Proofview.V82.tactic (tclEVARS sigma) <*>
     (Proofview.Goal.return v)
   in
@@ -1191,7 +1191,7 @@ and interp_tacarg ist arg =
       end la ((Proofview.Goal.return [])) >>== fun la_interp ->
       tac_of_old (fun gl -> interp_external loc ist { gl with sigma=project gl } com req la_interp)
   | TacFreshId l ->
-      Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) >>-- fun id ->
+      Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) >>== fun id ->
       (Proofview.Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)))
   | Tacexp t -> val_interp ist t
   | TacDynamic(_,t) ->
@@ -1324,11 +1324,11 @@ and interp_letin ist llc u =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-  Proofview.Goal.hyps >>-- fun hyps ->
+  Proofview.Goal.hyps >>== fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
   let hyps = if lr then List.rev hyps else hyps in
-  Proofview.Goal.concl >>-- fun concl ->
-  Proofview.Goal.env >>-- fun env ->
+  Proofview.Goal.concl >>== fun concl ->
+  Proofview.Goal.env >>== fun env ->
   let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
     let rec match_next_pattern next = match IStream.peek next with
     | None -> Proofview.tclZERO PatternMatchingFailure
@@ -1411,7 +1411,7 @@ and interp_match_goal ist lz lr lmr =
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
-  Proofview.Goal.env >>-- fun env ->
+  Proofview.Goal.env >>== fun env ->
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
     | hyp_pat::tl ->
 	let (hypname, _, pat as hyp_pat) =
@@ -1442,7 +1442,7 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
         in
         let init_match_pattern = Tacmach.New.of_old (fun gl ->
           apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) in
-        init_match_pattern >>-- match_next_pattern
+        init_match_pattern >>== match_next_pattern
     | [] ->
         let lfun = lfun +++ ist.lfun in
         let lfun = extend_values_with_bindings lmatch lfun in
@@ -1611,7 +1611,7 @@ and interp_match ist lz constr lmr =
     end
   end >>== fun csr ->
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>-- fun env ->
+  Proofview.Goal.env >>== fun env ->
   let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
   Proofview.tclORELSE
     (apply_match ist csr ilr)
@@ -1639,7 +1639,7 @@ and interp_ltac_constr ist e =
         | e -> Proofview.tclZERO e
       end
   end >>== fun result ->
-  Proofview.Goal.env >>-- fun env ->
+  Proofview.Goal.env >>== fun env ->
   let result = Value.normalize result in
   try
     let cresult = coerce_to_closed_constr env result in
@@ -1649,7 +1649,7 @@ and interp_ltac_constr ist e =
         pr_constr_env env cresult);
     (Proofview.Goal.return cresult)
   with CannotCoerceTo _ ->
-    Proofview.Goal.env >>-- fun env ->
+    Proofview.Goal.env >>== fun env ->
     Proofview.tclZERO (UserError ( "",
       errorlabstrm ""
       (str "Must evaluate to a closed term" ++ fnl() ++
@@ -1665,13 +1665,13 @@ and interp_atomic ist tac =
   match tac with
   (* Basic tactics *)
   | TacIntroPattern l ->
-      Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) >>- fun patterns ->
+      Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) >>= fun patterns ->
       h_intro_patterns patterns
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,hto) ->
-      Proofview.Goal.env >>- fun env ->
-      Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>- fun mloc ->
+      Proofview.Goal.env >>= fun env ->
+      Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
       h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
   | TacAssumption -> Proofview.V82.tactic h_assumption
   | TacExact c ->
@@ -1700,7 +1700,7 @@ and interp_atomic ist tac =
       end
   | TacApply (a,ev,cb,cl) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, l =
         List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
       in
@@ -1708,12 +1708,12 @@ and interp_atomic ist tac =
         | None -> fun l -> Proofview.V82.tactic (h_apply a ev l)
         | Some cl ->
             (fun l ->
-              Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>- fun cl ->
+              Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>= fun cl ->
               h_apply_in a ev l cl) in
       Tacticals.New.tclWITHHOLES ev tac sigma l
   | TacElim (ev,cb,cbo) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, cb = interp_constr_with_bindings ist env sigma cb in
       let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
       Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo
@@ -1727,7 +1727,7 @@ and interp_atomic ist tac =
       end
   | TacCase (ev,cb) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, cb = interp_constr_with_bindings ist env sigma cb in
       Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
   | TacCaseType c ->
@@ -1739,10 +1739,10 @@ and interp_atomic ist tac =
           gl
       end
   | TacFix (idopt,n) ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
   | TacMutualFix (id,n,l) ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         let f sigma (id,n,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
@@ -1759,10 +1759,10 @@ and interp_atomic ist tac =
           gl
       end
   | TacCofix idopt ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
   | TacMutualCofix (id,l) ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         let f sigma (id,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
@@ -1788,16 +1788,16 @@ and interp_atomic ist tac =
       end
   | TacAssert (t,ipat,c) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
-      Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>- fun patt ->
+      Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
       Tacticals.New.tclTHEN
 	(Proofview.V82.tactic (tclEVARS sigma))
         (Tactics.forward (Option.map (interp_tactic ist) t)
 	   (Option.map patt ipat) c)
   | TacGeneralize cl ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
         tclWITHHOLES false (h_generalize_gen) sigma cl gl
@@ -1812,12 +1812,11 @@ and interp_atomic ist tac =
       end
   | TacLetTac (na,c,clp,b,eqpat) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>- fun clp ->
-      Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>- fun eqpat ->
+      Proofview.Goal.env >>= fun env ->
+      Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp ->Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat ->
       if Locusops.is_nowhere clp then
         (* We try to fully-typecheck the term *)
-        Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
+        Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
 	Tacticals.New.tclTHEN
 	  (Proofview.V82.tactic (tclEVARS sigma))
           (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
@@ -1829,13 +1828,13 @@ and interp_atomic ist tac =
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Auto.h_trivial ~debug
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
   | TacAuto (debug,n,lems,l) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
@@ -1844,7 +1843,7 @@ and interp_atomic ist tac =
   | TacSimpleInductionDestruct (isrec,h) ->
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let l =
         Goal.sensitive_list_map begin fun (c,(ipato,ipats)) ->
           Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c ->
@@ -1857,10 +1856,10 @@ and interp_atomic ist tac =
         end l
       in
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.lift l >>- fun l ->
+      Proofview.Goal.lift l >>= fun l ->
       let sigma,el =
         Option.fold_map (interp_constr_with_bindings ist env) sigma el in
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>- fun interp_clause ->
+      Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause ->
       let cls = Option.map interp_clause cls in
       Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
   | TacDoubleInduction (h1,h2) ->
@@ -1868,24 +1867,24 @@ and interp_atomic ist tac =
       let h2 = interp_quantified_hypothesis ist h2 in
       Elim.h_double_induction h1 h2
   | TacDecomposeAnd c ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
+      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
 	(Proofview.V82.tactic (tclEVARS sigma))
 	(Elim.h_decompose_and c_interp)
   | TacDecomposeOr c ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
+      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
 	(Proofview.V82.tactic (tclEVARS sigma))
 	(Elim.h_decompose_or c_interp)
   | TacDecompose (l,c) ->
       let l = List.map (interp_inductive ist) l in
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
+      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
       Tacticals.New.tclTHEN
 	(Proofview.V82.tactic (tclEVARS sigma))
 	(Elim.h_decompose l c_interp)
   | TacSpecialize (n,cb) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         tclWITHHOLES false (h_specialize n) sigma cb gl
@@ -1913,7 +1912,7 @@ and interp_atomic ist tac =
         h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl
       end
   | TacRename l ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         h_rename (List.map (fun (id1,id2) ->
 	  interp_hyp ist gl id1,
@@ -1928,24 +1927,24 @@ and interp_atomic ist tac =
   (* Constructors *)
   | TacLeft (ev,bl) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, bl = interp_bindings ist env sigma bl in
       Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
   | TacRight (ev,bl) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, bl = interp_bindings ist env sigma bl in
       Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
   | TacSplit (ev,_,bll) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
       Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
   | TacAnyConstructor (ev,t) ->
       Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
   | TacConstructor (ev,n,bl) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let sigma, bl = interp_bindings ist env sigma bl in
       Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
 
@@ -1980,7 +1979,7 @@ and interp_atomic ist tac =
       end
   | TacChange (Some op,c,cl) ->
       Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       Proofview.V82.tactic begin fun gl -> 
         let sign,op = interp_typed_pattern ist env sigma op in
       (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
@@ -2002,13 +2001,13 @@ and interp_atomic ist tac =
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
   | TacSymmetry c ->
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl c) >>- fun cl ->
+      Tacmach.New.of_old (fun gl -> interp_clause ist gl c) >>= fun cl ->
       h_symmetry cl
   | TacTransitivity c ->
       begin match c with
       | None -> h_transitivity None
       | Some c ->
-          Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
+          Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
           Tacticals.New.tclTHEN
 	    (Proofview.V82.tactic (tclEVARS sigma))
 	    (h_transitivity (Some c_interp))
@@ -2019,7 +2018,7 @@ and interp_atomic ist tac =
       let l = List.map (fun (b,m,c) ->
         let f env sigma = interp_open_constr_with_bindings ist env sigma c in
 	(b,m,f)) l in
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) >>- fun cl ->
+      Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) >>= fun cl ->
       Equality.general_multi_multi_rewrite ev l cl
         (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
@@ -2029,24 +2028,24 @@ and interp_atomic ist tac =
       | Some c ->
           Goal.V82.to_sensitive (fun gl -> pf_interp_constr ist gl c) >- fun (sigma,c_interp) ->
 	  Goal.return (sigma , Some c_interp)
-      end >>- fun (sigma,c_interp) ->
-      Tacmach.New.of_old (interp_intro_pattern ist) >>- fun interp_intro_pattern ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps ->
+      end >>= fun (sigma,c_interp) ->
+      Tacmach.New.of_old (interp_intro_pattern ist) >>= fun interp_intro_pattern ->
+      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
       Inv.dinv k c_interp
         (Option.map interp_intro_pattern ids)
         dqhyps
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
-      Tacmach.New.of_old (interp_intro_pattern ist) >>- fun interp_intro_pattern ->
-      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>- fun hyps ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps ->
+      Tacmach.New.of_old (interp_intro_pattern ist) >>= fun interp_intro_pattern ->
+      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>= fun hyps ->
+      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
       Inv.inv_clause k
         (Option.map interp_intro_pattern ids)
         hyps
         dqhyps
   | TacInversion (InversionUsing (c,idl),hyp) ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps ->
-      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>- fun hyps ->
+      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
+      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>= fun hyps ->
       Leminv.lemInv_clause dqhyps
         c_interp
         hyps
@@ -2060,11 +2059,11 @@ and interp_atomic ist tac =
 	  let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in
 	  sigma , a_interp::acc
 	end l (goal_sigma,[])
-      end >>- fun (sigma,args) ->
+      end >>= fun (sigma,args) ->
       Proofview.V82.tactic (tclEVARS sigma) <*>
       tac args ist
   | TacAlias (loc,s,l,(_,body)) ->
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       let rec f x = match genarg_tag x with
           | IntOrVarArgType ->
               (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
@@ -2081,15 +2080,15 @@ and interp_atomic ist tac =
                                    (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
           | GenArgType -> f (out_gen (glbwit wit_genarg) x)
           | ConstrArgType ->
-              Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>-- fun (sigma,v) ->
+              Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>== fun (sigma,v) ->
               Proofview.V82.tactic (tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | OpenConstrArgType false ->
-              Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>-- fun (sigma,v) ->
+              Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>== fun (sigma,v) ->
               Proofview.V82.tactic (tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | ConstrMayEvalArgType ->
-              Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>-- fun (sigma,c_interp) ->
+              Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>== fun (sigma,c_interp) ->
               Proofview.V82.tactic (tclEVARS sigma) <*>
 	      Proofview.Goal.return (Value.of_constr c_interp)
           | ListArgType ConstrArgType ->
@@ -2099,7 +2098,7 @@ and interp_atomic ist tac =
 	          let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
 	          sigma , c_interp::acc
 	        end (out_gen wit x) (project gl,[])
-              end >>-- fun (sigma,l_interp) ->
+              end >>== fun (sigma,l_interp) ->
               Proofview.V82.tactic (tclEVARS sigma) <*>
               (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
           | ListArgType VarArgType ->
@@ -2135,7 +2134,7 @@ and interp_atomic ist tac =
                 Proofview.Goal.return v
               else
                 Tacmach.New.of_old (fun gl ->
-                  Geninterp.generic_interp ist gl x) >>-- fun (newsigma,v) ->
+                  Geninterp.generic_interp ist gl x) >>== fun (newsigma,v) ->
                 Proofview.V82.tactic (tclEVARS newsigma) <*>
                 Proofview.Goal.return v
           | QuantHypArgType | RedExprArgType
@@ -2172,7 +2171,7 @@ let eval_tactic t =
 
 let interp_tac_gen lfun avoid_ids debug t =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
   let ist = { lfun = lfun; extra = extra } in
@@ -2193,7 +2192,7 @@ let eval_ltac_constr t =
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 let hide_interp t ot =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
             gsigma = sigma; genv = env } in
   let te = intern_pure_tactic ist t in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ef6a0b19a0..b2405122ee 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -529,18 +529,18 @@ module New = struct
     Proofview.Goal.return (mkVar id)
 
   let onNthHypId m tac =
-    nthHypId m >>- tac
+    nthHypId m >>= tac
   let onNthHyp m tac =
-    nthHyp m >>- tac
+    nthHyp m >>= tac
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
 
-  let onNthDecl m tac = nthDecl m >>- tac
+  let onNthDecl m tac = nthDecl m >>= tac
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Tacmach.New.pf_get_hyp_typ id >>- fun typ ->
+    Tacmach.New.pf_get_hyp_typ id >>= fun typ ->
     if pred (id,typ) then
       tac1 id
     else
@@ -551,14 +551,14 @@ module New = struct
     Proofview.Goal.return (None :: List.map Option.make hyps)
 
   let tryAllHyps tac =
-    Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+    Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
     tclFIRST_PROGRESS_ON tac hyps
   let tryAllHypsAndConcl tac =
-    fullGoal >>- fun fullGoal ->
+    fullGoal >>= fun fullGoal ->
     tclFIRST_PROGRESS_ON tac fullGoal
 
   let onClause tac cl =
-    Tacmach.New.pf_ids_of_hyps >>- fun hyps ->
+    Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
 
   (* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -566,11 +566,11 @@ module New = struct
   let general_elim_then_using mk_elim
       isrec allnames tac predicate (indbindings,elimbindings)
       ind indclause =
-    Tacmach.New.of_old (mk_elim ind) >>- fun elim ->
+    Tacmach.New.of_old (mk_elim ind) >>= fun elim ->
     (* applying elimination_scheme just a little modified *)
     let indclause' = clenv_match_args indbindings indclause in
-    Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
-    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) >>- fun elimclause ->
+    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) >>= fun elimclause ->
     let indmv =
       match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -619,8 +619,8 @@ module New = struct
     new_elim_res_pf_THEN_i elimclause' branchtacs
 
   let elimination_then_using tac predicate bindings c =
-    Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>- fun (ind,t) ->
-    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>- fun indclause ->
+    Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>= fun (ind,t) ->
+    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
     let isrec,mkelim =
       if (Global.lookup_mind (fst ind)).mind_record
       then false,gl_make_case_dep
@@ -639,10 +639,10 @@ module New = struct
   let elimination_then tac        = elimination_then_using tac None
 
   let elim_on_ba tac ba =
-    Tacmach.New.of_old (make_elim_branch_assumptions ba) >>- fun branches ->
+    Tacmach.New.of_old (make_elim_branch_assumptions ba) >>= fun branches ->
     tac branches
 
   let case_on_ba tac ba = 
-    Tacmach.New.of_old (make_case_branch_assumptions ba) >>- fun branches ->
+    Tacmach.New.of_old (make_case_branch_assumptions ba) >>= fun branches ->
     tac branches
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ba1b2d9dcb..28d7268852 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -460,13 +460,13 @@ let build_intro_tac id dest tac = match dest with
   | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
 
 let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>= fun concl ->
   match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        find_name loc (name,None,t) name_flag >>- fun name ->
+        find_name loc (name,None,t) name_flag >>= fun name ->
 	build_intro_tac name move_flag tac
     | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        find_name loc (name,Some b,t) name_flag >>- fun name ->
+        find_name loc (name,Some b,t) name_flag >>= fun name ->
 	build_intro_tac name move_flag tac
     | _ ->
 	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -604,7 +604,7 @@ let depth_of_quantified_hypothesis red h gl =
 	  str".")
 
 let intros_until_gen red h =
-  Tacmach.New.of_old (depth_of_quantified_hypothesis red h) >>- fun n ->
+  Tacmach.New.of_old (depth_of_quantified_hypothesis red h) >>= fun n ->
   Tacticals.New.tclDO n (if red then introf else intro)
 
 let intros_until_id id = intros_until_gen true (NamedHyp id)
@@ -872,7 +872,7 @@ let find_eliminator c gl =
 (* arnaud: probable bug avec le try *)
 let default_elim with_evars (c,_ as cx) =
   Proofview.tclORELSE
-    (Tacmach.New.of_old (find_eliminator c) >>- fun elim ->
+    (Tacmach.New.of_old (find_eliminator c) >>= fun elim ->
      Proofview.V82.tactic (general_elim with_evars cx elim))
     begin function
       | IsRecord ->
@@ -1282,8 +1282,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if i > nconstr then error "Not enough constructors."
 
 let constructor_tac with_evars expctdnumopt i lbind =
-  Proofview.Goal.concl >>- fun cl ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
+  Proofview.Goal.concl >>= fun cl ->
+  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
   let (mind,redcl) = reduce_to_quantified_ind cl in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
@@ -1302,8 +1302,8 @@ let one_constructor i lbind = constructor_tac false None i lbind
 
 let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
-  Proofview.Goal.concl >>- fun cl ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>- fun reduce_to_quantified_ind ->
+  Proofview.Goal.concl >>= fun cl ->
+  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
   let mind = fst (reduce_to_quantified_ind cl) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
@@ -1379,7 +1379,7 @@ let intro_decomp_eq loc b l l' thin tac id gl =
 let intro_or_and_pattern loc b ll l' thin tac id =
   let c = mkVar id in
   Tacmach.New.of_old (fun gl ->
-    pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>- fun (ind,t) ->
+    pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>= fun (ind,t) ->
   let nv = mis_constr_nargs ind in
   let bracketed = b || not (List.is_empty l') in
   let adjust n l = if bracketed then adjust_intro_patterns n l else l in
@@ -1397,9 +1397,9 @@ let rewrite_hyp l2r id =
     Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
-  Proofview.Goal.env >>- fun env ->
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
-  Tacmach.New.pf_apply whd_betadeltaiota >>- fun whd_betadeltaiota ->
+  Proofview.Goal.env >>= fun env ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
   let t = whd_betadeltaiota (type_of (mkVar id)) in
   (* TODO: detect setoid equality? better detect the different equalities *)
   match match_with_equality_type t with
@@ -1564,10 +1564,10 @@ let clear_if_overwritten c ipats =
   | _ -> tclIDTAC
 
 let assert_as first ipat c =
-  Tacmach.New.of_old pf_hnf_type_of >>- fun hnf_type_of ->
+  Tacmach.New.of_old pf_hnf_type_of >>= fun hnf_type_of ->
   match kind_of_term (hnf_type_of c) with
   | Sort s ->
-      prepare_intros s ipat >>- fun (id,tac) ->
+      prepare_intros s ipat >>= fun (id,tac) ->
       let repl = not (Option.is_empty (allow_replace c ipat)) in
       Tacticals.New.tclTHENS
 	(Proofview.V82.tactic ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c))
@@ -1888,8 +1888,8 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
   (depdecls,lastlhyp,ccl,out test)
 
 let letin_tac_gen with_eq name (sigmac,c) test ty occs =
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.hyps >>- fun hyps ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
   let id =
     let t = match ty with Some t -> t | None -> typ_of env sigmac c in
@@ -1899,10 +1899,10 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
         if not (mem_named_context x hyps) then Goal.return x else
 	  error ("The variable "^(Id.to_string x)^" is already declared.")
       end in
-  id >>- fun id ->
-  Tacmach.New.of_old (letin_abstract id c test occs) >>- fun (depdecls,lastlhyp,ccl,c) ->
+  id >>= fun id ->
+  Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) ->
   let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
-  t >>- fun t ->
+  t >>= fun t ->
   let newcl = match with_eq with
     | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -1923,7 +1923,7 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
       end
     | None ->
 	(Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
-  newcl >>- fun (newcl,eq_tac) ->
+  newcl >>= fun (newcl,eq_tac) ->
   Tacticals.New.tclTHENLIST
     [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
       intro_gen dloc (IntroMustBe id) lastlhyp true false;
@@ -1938,7 +1938,7 @@ let letin_tac with_eq name c ty occs =
 
 let letin_pat_tac with_eq name c ty occs =
   Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>- fun env ->
+  Proofview.Goal.env >>= fun env ->
   letin_tac_gen with_eq name c
     (make_pattern_test env sigma c)
     ty (occs,true)
@@ -1947,7 +1947,7 @@ let letin_pat_tac with_eq name c ty occs =
 let forward usetac ipat c =
   match usetac with
   | None ->
-      Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+      Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
       let t = type_of c in
       Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
   | Some tac ->
@@ -2106,22 +2106,22 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
               let id' = next_ident_away (add_prefix "IH" id) avoid in
 	      (Proofview.Goal.return (pat, [dloc, IntroIdentifier id']))
           | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) in
-        recpat >>- fun (recpat,names) ->
+        recpat >>= fun (recpat,names) ->
         let dest = get_recarg_dest dests in
         safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
         let hyprec = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) in
-        hyprec >>- fun (hyprec,names) ->
+        hyprec >>= fun (hyprec,names) ->
 	safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
 	peel_tac ra' (update_dest dests ids') names thin))
     | (IndArg,dep,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) in
-        pat >>- fun (pat,names) ->
+        pat >>= fun (pat,names) ->
 	safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
     | (RecArg,dep,recvarname) :: ra' ->
         let pat = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) in
-        pat >>- fun (pat,names) ->
+        pat >>= fun (pat,names) ->
         let dest = get_recarg_dest dests in
 	safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
@@ -2145,8 +2145,8 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 (* Marche pas... faut prendre en compte l'occurrence précise... *)
 
 let atomize_param_of_ind (indref,nparams,_) hyp0 =
-  Tacmach.New.pf_get_hyp_typ hyp0 >>- fun tmptyp0 ->
-  Tacmach.New.pf_apply reduce_to_quantified_ref >>- fun reduce_to_quantified_ref ->
+  Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
+  Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
   let typ0 =  reduce_to_quantified_ref indref tmptyp0 in
   let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decompose_app indtyp) in
@@ -2154,27 +2154,27 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid =
     if not (Int.equal i nparams) then
-      Tacmach.New.pf_get_hyp_typ hyp0 >>- fun tmptyp0 ->
+      Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
       (* If argl <> [], we expect typ0 not to be quantified, in order to
          avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
-      Tacmach.New.pf_apply reduce_to_atomic_ref >>- fun reduce_to_atomic_ref ->
+      Tacmach.New.pf_apply reduce_to_atomic_ref >>= fun reduce_to_atomic_ref ->
       let indtyp = reduce_to_atomic_ref indref tmptyp0 in
       let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
-      Proofview.Goal.env >>- fun env ->
+      Proofview.Goal.env >>= fun env ->
       match kind_of_term c with
 	| Var id when not (List.exists (occur_var env id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid)
 	| Var id ->
-            Tacmach.New.of_old (fresh_id [] id) >>- fun x ->
+            Tacmach.New.of_old (fresh_id [] id) >>= fun x ->
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
 	| _ ->
-            Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+            Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
 	    let id = id_of_name_using_hdchar (Global.env()) (type_of c)
 		       Anonymous in
-            Tacmach.New.of_old (fresh_id [] id) >>- fun x ->
+            Tacmach.New.of_old (fresh_id [] id) >>= fun x ->
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
@@ -2657,7 +2657,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   if List.is_empty args then Proofview.tclUNIT ()
   else 
     let args = Array.of_list args in
-    Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) >>- fun newc ->
+    Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) >>= fun newc ->
       match newc with
       | None -> Proofview.tclUNIT ()
       | Some (newc, dep, n, vars) -> 
@@ -3099,7 +3099,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
    induction applies with the induction hypotheses *)
 
 let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names tac =
-  Tacmach.New.of_old (get_eliminator elim) >>- fun (isrec, elim, indsign) ->
+  Tacmach.New.of_old (get_eliminator elim) >>= fun (isrec, elim, indsign) ->
   let names = compute_induction_names (Array.length indsign) names in
   (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
     (Tacticals.New.tclTHEN
@@ -3111,8 +3111,8 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
    hypotheses from the context *)
 
 let apply_induction_in_context hyp0 elim indvars names induct_tac =
-  Proofview.Goal.env >>- fun env ->
-  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.concl >>= fun concl ->
   let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
   let deps = List.map (on_pi3 refresh_universes_strict) deps in
   let tmpcl = it_mkNamedProd_or_LetIn concl deps in
@@ -3192,8 +3192,8 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
 
 let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
-  Tacmach.New.pf_get_hyp_typ hyp0 >>- fun tmptyp0 ->
-  Tacmach.New.pf_apply reduce_to_quantified_ref >>- fun reduce_to_quantified_ref ->
+  Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
+  Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
   let typ0 = reduce_to_quantified_ref indref tmptyp0 in
   let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
@@ -3205,7 +3205,7 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
     (Some (hyp0,inhyps)) elim indvars names induct_tac
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
-  Tacmach.New.of_old (find_induction_type isrec elim hyp0) >>- fun elim_info ->
+  Tacmach.New.of_old (find_induction_type isrec elim hyp0) >>= fun elim_info ->
   Tacticals.New.tclTHEN
     (atomize_param_of_ind elim_info hyp0)
     (induction_from_context isrec with_evars elim_info
@@ -3215,7 +3215,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin
    scheme (which is mandatory for multiple ind args), check that all
    parameters and arguments are given (mandatory too). *)
 let induction_without_atomization isrec with_evars elim names lid =
-  Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) >>- fun (indsign,scheme as elim_info) ->
+  Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) >>= fun (indsign,scheme as elim_info) ->
   let awaited_nargs =
     scheme.nparams + scheme.nargs
     + (if scheme.farg_in_concl then 1 else 0)
@@ -3269,14 +3269,14 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	    isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
         Proofview.tclEVARMAP >= fun defs ->
-        Proofview.Goal.env >>- fun env ->
+        Proofview.Goal.env >>= fun env ->
 	let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
 		  Anonymous in
-        Tacmach.New.of_old (fresh_id [] x) >>- fun id ->
+        Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
 	(* We need the equality name now *)
 	let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
-        Proofview.Goal.env >>- fun env ->
+        Proofview.Goal.env >>= fun env ->
 	Tacticals.New.tclTHEN
           (* Warning: letin is buggy when c is not of inductive type *)
 	  (letin_tac_gen with_eq (Name id) (sigma,c)
@@ -3307,11 +3307,11 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 		atomize_list l'
 
 	    | _ ->
-                Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+                Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
 		let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
-                Tacmach.New.of_old (fresh_id [] x) >>- fun id ->
+                Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
 		let newl' = List.map (replace_term c (mkVar id)) l' in
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
@@ -3336,7 +3336,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
    args *)
 let induct_destruct isrec with_evars (lc,elim,names,cls) =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
-  Tacmach.New.of_old (is_functional_induction elim) >>- fun ifi ->
+  Tacmach.New.of_old (is_functional_induction elim) >>= fun ifi ->
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
@@ -3351,7 +3351,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
       str "Example: induction x1 x2 x3 using my_scheme.");
     if not (Option.is_empty cls) then
       error "'in' clause not supported here.";
-    Tacmach.New.pf_apply finish_evar_resolution >>- fun finish_evar_resolution ->
+    Tacmach.New.pf_apply finish_evar_resolution >>= fun finish_evar_resolution ->
     let lc = List.map
       (map_induction_arg finish_evar_resolution) lc in
     begin match lc with
@@ -3460,8 +3460,8 @@ let case_type t gl =
  *)
 
 let andE id =
-  Tacmach.New.pf_get_hyp_typ id >>- fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>- fun hnf_constr ->
+  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
+  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
   if is_conjunction (hnf_constr t) then
     (Tacticals.New.tclTHEN (simplest_elim (mkVar id)) (Tacticals.New.tclDO 2 intro))
   else
@@ -3476,8 +3476,8 @@ let dAnd cls =
     cls
 
 let orE id =
-  Tacmach.New.pf_get_hyp_typ id >>- fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>- fun hnf_constr ->
+  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
+  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
   if is_disjunction (hnf_constr t) then
     (Tacticals.New.tclTHEN (simplest_elim (mkVar id)) intro)
   else
@@ -3492,8 +3492,8 @@ let dorE b cls =
     cls
 
 let impE id =
-  Tacmach.New.pf_get_hyp_typ id >>- fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>- fun hnf_constr ->
+  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
+  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
   if is_imp_term (hnf_constr t) then
     let (dom, _, rng) = destProd (hnf_constr t) in
     Tacticals.New.tclTHENLAST
@@ -3530,7 +3530,7 @@ let reflexivity_red allowred =
       Goal.defs >- fun sigma ->
       Goal.return (whd_betadeltaiota env sigma c)
   in
-  Proofview.Goal.lift concl >>- fun concl ->
+  Proofview.Goal.lift concl >>= fun concl ->
     match match_with_equality_type concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
@@ -3587,7 +3587,7 @@ let symmetry_red allowred =
       Goal.defs >- fun sigma ->
       Goal.return (whd_betadeltaiota env sigma c)
   in
-  Proofview.Goal.lift concl >>- fun concl ->
+  Proofview.Goal.lift concl >>= fun concl ->
   match_with_equation concl >= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
@@ -3610,7 +3610,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 
 let symmetry_in id =
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   let ctype = type_of (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
@@ -3665,7 +3665,7 @@ let prove_transitivity hdcncl eq_kind t =
       Goal.return 
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
-  end >>- fun (eq1,eq2) ->
+  end >>= fun (eq1,eq2) ->
   Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq2))
     (Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq1))
        (Tacticals.New.tclTHENLIST
@@ -3686,7 +3686,7 @@ let transitivity_red allowred t =
       Goal.defs >- fun sigma ->
       Goal.return (whd_betadeltaiota env sigma c)
   in
-  Proofview.Goal.lift concl >>- fun concl ->
+  Proofview.Goal.lift concl >>= fun concl ->
   match_with_equation concl >= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->