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

1 files changed, 20 insertions, 20 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index e120de478..06c9f8793 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -246,7 +246,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
 let _M =mkMeta
 
 let rec proof_tac p : unit Proofview.tactic =
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   match p.p_rule with
       Ax c -> Proofview.V82.tactic (exact_check c)
     | SymAx c ->
@@ -280,7 +280,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	let typf = Termops.refresh_universes (type_of tf1) in
 	let typx = Termops.refresh_universes (type_of tx1) in
 	let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in
-        Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) >>- fun id ->
+        Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) >>= fun id ->
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
@@ -309,28 +309,28 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let intype = Termops.refresh_universes (type_of ti) in
 	 let outtype = Termops.refresh_universes (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
-         Tacmach.New.of_old (build_projection intype outtype cstr special default) >>- fun proj ->
+         Tacmach.New.of_old (build_projection intype outtype cstr special default) >>= fun proj ->
 	 let injt=
 	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
 	   Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf)
 
 let refute_tac c t1 t2 p =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) >>- fun intype ->
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) >>= fun intype ->
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>- fun hid ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
   let false_t=mkApp (c,[|mkVar hid|]) in
     Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
       [proof_tac p; simplest_elim false_t]
 
 let convert_to_goal_tac c t1 t2 p = 
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) >>- fun sort ->
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) >>= fun sort ->
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) >>- fun e ->
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun x ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) >>= fun e ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun x ->
   let identity=mkLambda (Name x,sort,mkRel 1) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
@@ -339,7 +339,7 @@ let convert_to_goal_tac c t1 t2 p =
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
   let tt2=constr_of_term t2 in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>- fun h ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>= fun h ->
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
@@ -347,17 +347,17 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
 
 let discriminate_tac cstr p =
   let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>- fun intype ->
-  Proofview.Goal.concl >>- fun concl ->
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype ->
+  Proofview.Goal.concl >>= fun concl ->
   let outsort = mkType (Termops.new_univ ()) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun xid ->
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>- fun tid ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid ->
   let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
-  Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>- fun trivial ->
+  Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial ->
   let outtype = mkType (Termops.new_univ ()) in
   let pred=mkLambda(Name xid,outtype,mkRel 1) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>- fun hid ->
-  Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>- fun proj ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
+  Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj ->
   let injt=mkApp (Lazy.force _f_equal,
 		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
   let endt=mkApp (Lazy.force _eq_rect,
@@ -379,7 +379,7 @@ let cc_tactic depth additionnal_terms =
   Proofview.tclUNIT () >= fun () -> (* delay for check_required_library *)
   Coqlib.check_required_library Coqlib.logic_module_name;
   let _ = debug (Pp.str "Reading subgoal ...") in
-  Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>- fun state ->
+  Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state ->
   let _ = debug (Pp.str "Problem built, solving ...") in
   let sol = execute true state in
   let _ = debug (Pp.str "Computation completed.") in
@@ -394,7 +394,7 @@ let cc_tactic depth additionnal_terms =
 		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 		discriminate_tac cstr p
 	    | Incomplete ->
-                Proofview.Goal.env >>- fun env ->
+                Proofview.Goal.env >>= fun env ->
 		let metacnt = ref 0 in
 		let newmeta _ = incr metacnt; _M !metacnt in
 		let terms_to_complete =
@@ -451,8 +451,8 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 *)
 
 let f_equal =
-  Proofview.Goal.concl >>- fun concl ->
-  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Proofview.Goal.concl >>= fun concl ->
+  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   let cut_eq c1 c2 =
     let ty = Termops.refresh_universes (type_of c1) in
     Proofview.V82.tactic begin