aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/cc/cctac.ml40
-rw-r--r--plugins/omega/coq_omega.ml28
-rw-r--r--plugins/quote/quote.ml18
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/proofview.ml8
-rw-r--r--proofs/proofview.mli17
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/contradiction.ml12
-rw-r--r--tactics/elim.ml8
-rw-r--r--tactics/eqdecide.ml416
-rw-r--r--tactics/equality.ml60
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--tactics/extratactics.ml420
-rw-r--r--tactics/inv.ml24
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/refine.ml4
-rw-r--r--tactics/rewrite.ml33
-rw-r--r--tactics/tacinterp.ml127
-rw-r--r--tactics/tacticals.ml28
-rw-r--r--tactics/tactics.ml122
-rw-r--r--toplevel/auto_ind_decl.ml38
25 files changed, 319 insertions, 326 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4585468ad..440309284 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,7 +217,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>= fun concl ->
let eq = Lazy.force eq in
let t = decomp_term concl in
match t with
@@ -230,7 +230,7 @@ module Btauto = struct
Tacticals.New.tclFAIL 0 msg
let tac =
- Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>= fun concl ->
let eq = Lazy.force eq in
let bool = Lazy.force Bool.typ in
let t = decomp_term concl in
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
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index adc1d9ee3..70c6d2212 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -35,7 +35,7 @@ open OmegaSolver
(* Added by JCF, 09/03/98 *)
let elim_id id =
- Tacmach.New.pf_global id >>- fun c ->
+ Tacmach.New.pf_global id >>= fun c ->
simplest_elim c
let resolve_id id gl = apply (pf_global gl id) gl
@@ -1381,8 +1381,8 @@ open Proofview.Notations
let coq_omega =
Proofview.tclUNIT () >= fun () -> (* delay for the effects in [clear_tables] *)
clear_tables ();
- Tacmach.New.pf_hyps_types >>- fun hyps_types ->
- Tacmach.New.of_old destructure_omega >>- fun destructure_omega ->
+ Tacmach.New.pf_hyps_types >>= fun hyps_types ->
+ Tacmach.New.of_old destructure_omega >>= fun destructure_omega ->
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1431,7 +1431,7 @@ let coq_omega =
let coq_omega = coq_omega
let nat_inject =
- Tacmach.New.pf_apply Reductionops.is_conv >>- fun is_conv ->
+ Tacmach.New.pf_apply Reductionops.is_conv >>= fun is_conv ->
let rec explore p t : unit Proofview.tactic =
try match destructurate_term t with
| Kapp(Plus,[t1;t2]) ->
@@ -1562,7 +1562,7 @@ let nat_inject =
| _ -> loop lit
with e when catchable_exception e -> loop lit end
in
- Tacmach.New.pf_hyps_types >>- fun hyps_types ->
+ Tacmach.New.pf_hyps_types >>= fun hyps_types ->
loop (List.rev hyps_types)
let dec_binop = function
@@ -1633,20 +1633,20 @@ let onClearedName id tac =
(* so renaming may be necessary *)
Tacticals.New.tclTHEN
(Proofview.V82.tactic (tclTRY (clear [id])))
- (Tacmach.New.of_old (fresh_id [] id) >>- fun id ->
+ (Tacmach.New.of_old (fresh_id [] id) >>= fun id ->
Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id))
let onClearedName2 id tac =
Tacticals.New.tclTHEN
(Proofview.V82.tactic (tclTRY (clear [id])))
- (Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) >>- fun id1 ->
- Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) >>- fun id2 ->
+ (Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) >>= fun id1 ->
+ Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) >>= fun id2 ->
Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ])
let destructure_hyps =
- Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
- Tacmach.New.of_old decidability >>- fun decidability ->
- Tacmach.New.of_old pf_nf >>- fun pf_nf ->
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ Tacmach.New.of_old decidability >>= fun decidability ->
+ Tacmach.New.of_old pf_nf >>= fun pf_nf ->
let rec loop = function
| [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
| (i,body,t)::lit ->
@@ -1781,12 +1781,12 @@ let destructure_hyps =
| e when catchable_exception e -> loop lit
end
in
- Proofview.Goal.hyps >>- fun hyps ->
+ Proofview.Goal.hyps >>= fun hyps ->
loop (Environ.named_context_of_val hyps)
let destructure_goal =
- Proofview.Goal.concl >>- fun concl ->
- Tacmach.New.of_old decidability >>- fun decidability ->
+ Proofview.Goal.concl >>= fun concl ->
+ Tacmach.New.of_old decidability >>= fun decidability ->
let rec loop t =
match destructurate_prop t with
| Kapp(Not,[t]) ->
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 80053ea4d..bf061095c 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -453,11 +453,11 @@ let quote_terms ivs lc =
yet. *)
let quote f lid =
- Tacmach.New.pf_global f >>- fun f ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
- Proofview.Goal.lift (compute_ivs f cl) >>- fun ivs ->
- Proofview.Goal.concl >>- fun concl ->
- Proofview.Goal.lift (quote_terms ivs [concl]) >>- fun quoted_terms ->
+ Tacmach.New.pf_global f >>= fun f ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+ Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
+ Proofview.Goal.concl >>= fun concl ->
+ Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
@@ -467,10 +467,10 @@ let quote f lid =
| Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
let gen_quote cont c f lid =
- Tacmach.New.pf_global f >>- fun f ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
- Proofview.Goal.lift (compute_ivs f cl) >>- fun ivs ->
- Proofview.Goal.lift (quote_terms ivs [c]) >>- fun quoted_terms ->
+ Tacmach.New.pf_global f >>= fun f ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+ Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
+ Proofview.Goal.lift (quote_terms ivs [c]) >>= fun quoted_terms ->
let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 011aba5d7..010a550f0 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -799,7 +799,7 @@ open Proofview.Notations
let ring_lookup (f:glob_tactic_expr) lH rl t =
Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.env >>= fun env ->
let rl = make_args_list rl t in
let e = find_ring_structure env sigma rl in
let rl = carg (make_term_list e.ring_carrier rl) in
@@ -1120,7 +1120,7 @@ let ltac_field_structure e =
let field_lookup (f:glob_tactic_expr) lH rl t =
Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>- fun env ->
+ Proofview.Goal.env >>= fun env ->
let rl = make_args_list rl t in
let e = find_field_structure env sigma rl in
let rl = carg (make_term_list e.field_carrier rl) in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 76cf41c50..7874f5ac6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -85,7 +85,7 @@ let elim_res_pf_THEN_i clenv tac gls =
open Proofview.Notations
let new_elim_res_pf_THEN_i clenv tac =
- Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>- fun clenv' ->
+ Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>= fun clenv' ->
Proofview.tclTHEN
(Proofview.V82.tactic (clenv_refine false clenv'))
(Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bac4c22cd..406de8d2b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -168,7 +168,7 @@ let unfocus c sp =
meta-level as OCaml functions.
Most tactics, in the sense we are used to, return [ () ], that is
no really interesting values. But some might pass information
- around; the [(>>--)] and [(>>==)] bind-like construction are the
+ around; the [(>>==)] and [(>>==)] bind-like construction are the
main ingredients of this information passing.
(* spiwack: I don't know how much all this relates to F. Kirchner and
C. Muñoz. I wasn't able to understand how they used the monad
@@ -409,7 +409,7 @@ type 'a glist = 'a list
module Notations = struct
let (>-) = Goal.bind
let (>=) = tclBIND
- let (>>-) t k =
+ let (>>=) t k =
(* spiwack: the application of List.map may raise errors, as this
combinator is mostly used in porting historical tactic code,
where the error flow is somewhat hard to follow, hence the
@@ -417,7 +417,7 @@ module Notations = struct
t >= fun l ->
try tclDISPATCH (List.map k l)
with e when Errors.noncritical e -> tclZERO e
- let (>>--) t k =
+ let (>>==) t k =
(* spiwack: the application of List.map may raise errors, as this
combinator is mostly used in porting historical tactic code,
where the error flow is somewhat hard to follow, hence the
@@ -428,8 +428,6 @@ module Notations = struct
with e when Errors.noncritical e -> tclZERO e
end >= fun l' ->
tclUNIT (List.flatten l')
- let (>>=) = (>>-)
- let (>>==) = (>>--)
let (<*>) = tclTHEN
let (<+>) t1 t2 = tclOR t2 (fun _ -> t2)
end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 261311592..2a69ccaf3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -212,21 +212,16 @@ type 'a glist = private 'a list
module Notations : sig
(* Goal.bind *)
val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
- (* [t >>- k] is [tclBIND t (fun l -> tclDISPATCH (List.map k l))] *)
- val (>>-) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
- (* arnaud: commenter *)
- val (>>--) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
(* tclBIND *)
val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-
- (* arnaud: commentaire à mettre à jour *)
- (* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
- tactic monad and the goal-sensitive monad.
- It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
- needs a bind, since it usually avoids to delay the interpretation of the
- goal sensitive value to a location where it does not make sense anymore. *)
+ (* [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
+ corresponding goal. *)
val (>>=) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
+ (* [t >>== k] acts as [t] except that [k] returns a list of value
+ corresponding to its produced subgoals. *)
val (>>==) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
(* tclTHEN *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8115376c9..fd6dd0361 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 8a09ff789..9c1f462ba 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 f1ebdc638..0725825e9 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 ed1661910..7904c88ee 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 a784264f0..f8f85ef3c 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 cc6547bc3..0a6e7a072 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 0ad306aba..a7b04bee2 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 80b06b2fb..0555564bd 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 71b2bdfb6..a37880170 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 644f527a0..8e551d3f3 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 786f92736..06b067fcf 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 61db456dd..d0ef1ec2e 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 fb9ca2507..30fe8d4ae 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 d788ade4d..1c5903d51 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 ef6a0b19a..b2405122e 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 ba1b2d9dc..28d726885 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,_,_ ->
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b37dd0398..f35a34633 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -351,7 +351,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
)))
)
in
- Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
let type_of_pq = type_of p in
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
@@ -411,7 +411,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
- Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
let tt1 = type_of t1 in
if eq_constr t1 t2 then aux q1 q2
else (
@@ -557,11 +557,11 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end
in
- Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros ->
let fresh_id s = Proofview.Goal.lift (fresh_id s) in
- fresh_id (Id.of_string "x") >>- fun freshn ->
- fresh_id (Id.of_string "y") >>- fun freshm ->
- fresh_id (Id.of_string "Z") >>- fun freshz ->
+ fresh_id (Id.of_string "x") >>= fun freshn ->
+ fresh_id (Id.of_string "y") >>= fun freshm ->
+ fresh_id (Id.of_string "Z") >>= fun freshz ->
(* try with *)
Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
intro_using freshn ;
@@ -580,7 +580,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
simple_apply_in freshz (andb_prop());
- fresh_id (Id.of_string "Z") >>- fun fresht ->
+ fresh_id (Id.of_string "Z") >>= fun fresht ->
(new_destruct false [Tacexpr.ElimOnConstr
(Evd.empty,((mkVar freshz,NoBindings)))]
None
@@ -592,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.concl >>- fun gl ->
+ Proofview.Goal.concl >>= fun gl ->
match (kind_of_term gl) with
| App (c,ca) -> (
match (kind_of_term c) with
@@ -688,11 +688,11 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end
in
- Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros ->
let fresh_id s = Proofview.Goal.lift (fresh_id s) in
- fresh_id (Id.of_string "x") >>- fun freshn ->
- fresh_id (Id.of_string "y") >>- fun freshm ->
- fresh_id (Id.of_string "Z") >>- fun freshz ->
+ fresh_id (Id.of_string "x") >>= fun freshn ->
+ fresh_id (Id.of_string "y") >>= fun freshm ->
+ fresh_id (Id.of_string "Z") >>= fun freshz ->
(* try with *)
Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
intro_using freshn ;
@@ -711,7 +711,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.concl >>- fun gl ->
+ Proofview.Goal.concl >>= fun gl ->
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
| App(c,ca) -> (match (kind_of_term ca.(1)) with
@@ -826,11 +826,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end
in
- Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>- fun fresh_first_intros ->
+ Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros ->
let fresh_id s = Proofview.Goal.lift (fresh_id s) in
- fresh_id (Id.of_string "x") >>- fun freshn ->
- fresh_id (Id.of_string "y") >>- fun freshm ->
- fresh_id (Id.of_string "H") >>- fun freshH ->
+ fresh_id (Id.of_string "x") >>= fun freshn ->
+ fresh_id (Id.of_string "y") >>= fun freshm ->
+ fresh_id (Id.of_string "H") >>= fun freshH ->
let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
let arfresh = Array.of_list fresh_first_intros in
let xargs = Array.sub arfresh 0 (2*nparrec) in
@@ -860,7 +860,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
)
(Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
- fresh_id (Id.of_string "H") >>- fun freshH2 ->
+ fresh_id (Id.of_string "H") >>= fun freshH2 ->
Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
(* left *)
Tacticals.New.tclTHENLIST [
@@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
];
(*right *)
- fresh_id (Id.of_string "H") >>- fun freshH3 ->
+ fresh_id (Id.of_string "H") >>= fun freshH3 ->
Tacticals.New.tclTHENLIST [
simplest_right ;
Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref));
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 18:40:55 +0000