aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/omega/coq_omega.ml2
-rw-r--r--proofs/proofview.ml12
-rw-r--r--proofs/proofview.mli2
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/eqdecide.ml46
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/tacinterp.ml72
-rw-r--r--tactics/tacticals.ml14
-rw-r--r--tactics/tactics.ml12
-rw-r--r--toplevel/auto_ind_decl.ml14
13 files changed, 74 insertions, 74 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c125be65a..563148872 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -141,7 +141,7 @@ END
open Proofview.Notations
let default_declarative_automation =
- Proofview.tclUNIT () >= fun () -> (* delay for [congruence_depth] *)
+ Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
Tacticals.New.tclORELSE
(Tacticals.New.tclORELSE (Auto.h_trivial [] None)
(Cctac.congruence_tac !congruence_depth []))
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index b61279cd5..74f1ba713 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1861,7 +1861,7 @@ let destructure_goal =
let destructure_goal = destructure_goal
let omega_solver =
- Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
+ Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *)
Coqlib.check_required_library ["Coq";"omega";"Omega"];
reset_all ();
destructure_goal
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d42ea8b80..0dbbdca7c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -641,7 +641,7 @@ let in_proofview p k =
module Notations = struct
- let (>=) = tclBIND
+ let (>>=) = tclBIND
let (<*>) = tclTHEN
let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
end
@@ -650,8 +650,8 @@ open Notations
let rec list_map f = function
| [] -> tclUNIT []
| a::l ->
- f a >= fun a' ->
- list_map f l >= fun l' ->
+ f a >>= fun a' ->
+ list_map f l >>= fun l' ->
tclUNIT (a'::l')
@@ -807,8 +807,8 @@ module Goal = struct
end
let enter f =
list_iter_goal () begin fun goal () ->
- Proof.current >= fun env ->
- tclEVARMAP >= fun sigma ->
+ Proof.current >>= fun env ->
+ tclEVARMAP >>= fun sigma ->
try
(* enter_t cannot modify the sigma. *)
let (t,_) = Goal.eval (enter_t f) env sigma goal in
@@ -822,7 +822,7 @@ module Goal = struct
(* compatibility *)
let goal { self=self } = self
let refresh_sigma g =
- tclEVARMAP >= fun sigma ->
+ tclEVARMAP >>= fun sigma ->
tclUNIT { g with sigma }
end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index c608bc841..60a6c558c 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -270,7 +270,7 @@ val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
module Notations : sig
(* tclBIND *)
- val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+ val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
(* [t >>= k] is [t >= fun l -> tclDISPATCH (List.map k l)].
The [t] is supposed to return a list of values of the size of the
list of goals. [k] is then applied to each of this value in the
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74a1c5624..61e7dde18 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 f5f09f27e..81fab6e2b 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 a98cb2a6f..4b1cd8715 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 033a4dc1b..a397976ea 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 fb6de660d..06853e137 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 171c24858..3d0c65862 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 639c4c97b..c6a3a0012 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 b4b6934f2..fe26bbb2d 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
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 1173a2510..b79d77443 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -370,7 +370,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
in
Proofview.tclZERO (Errors.UserError("",err_msg))
in
- lb_type_of_p >= fun (lb_type_of_p,eff) ->
+ lb_type_of_p >>= fun (lb_type_of_p,eff) ->
let lb_args = Array.append (Array.append
(Array.map (fun x -> x) v)
(Array.map (fun x -> do_arg x 1) v))
@@ -463,22 +463,22 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
in
begin try Proofview.tclUNIT (destApp lft)
with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
- end >= fun (ind1,ca1) ->
+ end >>= fun (ind1,ca1) ->
begin try Proofview.tclUNIT (destApp rgt)
with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
- end >= fun (ind2,ca2) ->
+ end >>= fun (ind2,ca2) ->
begin try Proofview.tclUNIT (destInd ind1)
with DestKO ->
begin try Proofview.tclUNIT (fst (destConstruct ind1))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
- end >= fun (sp1,i1) ->
+ end >>= fun (sp1,i1) ->
begin try Proofview.tclUNIT (destInd ind2)
with DestKO ->
begin try Proofview.tclUNIT (fst (destConstruct ind2))
with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
end
- end >= fun (sp2,i2) ->
+ end >>= fun (sp2,i2) ->
if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type"))
else aux (Array.to_list ca1) (Array.to_list ca2)
@@ -854,14 +854,14 @@ let compute_dec_tact ind lnamesparrec nparrec =
Not_found ->
Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++
str" equality is required."))
- end >= fun (blI,eff') ->
+ end >>= fun (blI,eff') ->
begin try
let c, eff = find_scheme lb_scheme_kind ind in
Proofview.tclUNIT (mkConst c,eff) with
Not_found ->
Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
str" equality is required."))
- end >= fun (lbI,eff'') ->
+ end >>= fun (lbI,eff'') ->
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (Tactics.emit_side_effects
(Declareops.union_side_effects eff''
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 01:03:35 +0000