aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
5 files changed, 47 insertions, 47 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 22:33:27 +0000