diff options
author | 2014-02-27 12:54:29 +0100 | |
---|---|---|
committer | 2014-02-27 12:55:37 +0100 | |
commit | 27d780bd52e1776afb05793d43ac030af861c82d (patch) | |
tree | b4136cb61e89a2f3c6cef9323fa697dceed4f3c2 | |
parent | 0a1c88bb9400cb16c3dba827e641086215497e8c (diff) |
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Impacts MapleMode.
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
-rw-r--r-- | proofs/proofview.ml | 12 | ||||
-rw-r--r-- | proofs/proofview.mli | 2 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/elim.ml | 2 | ||||
-rw-r--r-- | tactics/eqdecide.ml4 | 6 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
-rw-r--r-- | tactics/inv.ml | 4 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 72 | ||||
-rw-r--r-- | tactics/tacticals.ml | 14 | ||||
-rw-r--r-- | tactics/tactics.ml | 12 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 14 |
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'' |