aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/cc/cctac.ml50
-rw-r--r--plugins/omega/coq_omega.ml40
-rw-r--r--plugins/quote/quote.ml10
-rw-r--r--proofs/clenvtac.ml10
-rw-r--r--proofs/goal.ml4
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/proofview.ml28
-rw-r--r--proofs/proofview.mli4
-rw-r--r--proofs/tacmach.ml85
-rw-r--r--proofs/tacmach.mli34
-rw-r--r--tactics/auto.ml25
-rw-r--r--tactics/autorewrite.ml10
-rw-r--r--tactics/contradiction.ml8
-rw-r--r--tactics/elim.ml10
-rw-r--r--tactics/eqdecide.ml420
-rw-r--r--tactics/equality.ml89
-rw-r--r--tactics/extratactics.ml416
-rw-r--r--tactics/inv.ml30
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--tactics/tacinterp.ml170
-rw-r--r--tactics/tacticals.ml40
-rw-r--r--tactics/tactics.ml226
-rw-r--r--toplevel/auto_ind_decl.ml8
24 files changed, 555 insertions, 370 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index dee57cd04..0d1238814 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -246,7 +246,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
try (* type_of can raise exceptions *)
match p.p_rule with
Ax c -> Proofview.V82.tactic (exact_check c)
@@ -281,7 +282,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 ->
+ let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
mkApp(Lazy.force _f_equal,
@@ -310,57 +311,72 @@ 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 ->
+ let proj =
+ Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
+ in
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)
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let refute_tac c t1 t2 p =
+ Proofview.Goal.enter begin fun gl ->
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 ->
+ let intype =
+ Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) gl
+ in
let neweq=
mkApp(Lazy.force _eq,
[|intype;tt1;tt2|]) in
- Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
+ let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
let false_t=mkApp (c,[|mkVar hid|]) in
Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
[proof_tac p; simplest_elim false_t]
+ end
let convert_to_goal_tac c t1 t2 p =
+ Proofview.Goal.enter begin fun gl ->
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 ->
+ let sort =
+ Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) gl
+ in
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 ->
+ let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+ let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
let identity=mkLambda (Name x,sort,mkRel 1) in
let endt=mkApp (Lazy.force _eq_rect,
[|sort;tt1;identity;c;tt2;mkVar e|]) in
Tacticals.New.tclTHENS (assert_tac (Name e) neweq)
[proof_tac p; Proofview.V82.tactic (exact_check endt)]
+ end
let convert_to_hyp_tac c1 t1 c2 t2 p =
+ Proofview.Goal.enter begin fun gl ->
let tt2=constr_of_term t2 in
- Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>= fun h ->
+ let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
let false_t=mkApp (c2,[|mkVar h|]) in
Tacticals.New.tclTHENS (assert_tac (Name h) tt2)
[convert_to_goal_tac c1 t1 t2 p;
simplest_elim false_t]
+ end
let discriminate_tac cstr p =
Proofview.Goal.enter begin fun gl ->
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 ->
+ let intype =
+ Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) gl
+ in
let concl = Proofview.Goal.concl gl in
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 ->
+ let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+ let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in
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 ->
+ let trivial = Tacmach.New.of_old (fun gls -> pf_type_of gls identity) gl in
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 ->
+ let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+ let proj = Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) gl in
let injt=mkApp (Lazy.force _f_equal,
[|intype;outtype;proj;t1;t2;mkVar hid|]) in
let endt=mkApp (Lazy.force _eq_rect,
@@ -383,7 +399,7 @@ let cc_tactic depth additionnal_terms =
Proofview.Goal.enter begin fun gl ->
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 ->
+ let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
let _ = debug (Pp.str "Problem built, solving ...") in
let sol = execute true state in
let _ = debug (Pp.str "Computation completed.") in
@@ -457,7 +473,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
let f_equal =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
let ty = Termops.refresh_universes (type_of c1) in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c865639e6..a647238bf 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -35,8 +35,9 @@ open OmegaSolver
(* Added by JCF, 09/03/98 *)
let elim_id id =
- Tacmach.New.pf_global id >>= fun c ->
- simplest_elim c
+ Proofview.Goal.enter begin fun gl ->
+ simplest_elim (Tacmach.New.pf_global id gl)
+ end
let resolve_id id gl = apply (pf_global gl id) gl
let timing timer_name f arg = f arg
@@ -1379,10 +1380,10 @@ let reintroduce id =
open Proofview.Notations
let coq_omega =
- Proofview.tclUNIT () >= fun () -> (* delay for the effects in [clear_tables] *)
+ Proofview.Goal.enter begin fun gl ->
clear_tables ();
- Tacmach.New.pf_hyps_types >>= fun hyps_types ->
- Tacmach.New.of_old destructure_omega >>= fun destructure_omega ->
+ let hyps_types = Tacmach.New.pf_hyps_types gl in
+ let destructure_omega = Tacmach.New.of_old destructure_omega gl in
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1427,11 +1428,13 @@ let coq_omega =
Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
end
+ end
let coq_omega = coq_omega
let nat_inject =
- Tacmach.New.pf_apply Reductionops.is_conv >>= fun is_conv ->
+ Proofview.Goal.enter begin fun gl ->
+ let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
let rec explore p t : unit Proofview.tactic =
try match destructurate_term t with
| Kapp(Plus,[t1;t2]) ->
@@ -1562,8 +1565,9 @@ let nat_inject =
| _ -> loop lit
with e when catchable_exception e -> loop lit end
in
- Tacmach.New.pf_hyps_types >>= fun hyps_types ->
+ let hyps_types = Tacmach.New.pf_hyps_types gl in
loop (List.rev hyps_types)
+ end
let dec_binop = function
| Zne -> coq_dec_Zne
@@ -1633,21 +1637,25 @@ 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 ->
- Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id))
+ (Proofview.Goal.enter begin fun gl ->
+ let id = Tacmach.New.of_old (fresh_id [] id) gl in
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
+ end)
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 ->
- Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ])
+ (Proofview.Goal.enter begin fun gl ->
+ let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
+ let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
+ Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ]
+ end)
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 ->
Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+ let decidability = Tacmach.New.of_old decidability gl in
+ let pf_nf = Tacmach.New.of_old pf_nf gl in
let rec loop = function
| [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
| (i,body,t)::lit ->
@@ -1791,7 +1799,7 @@ let destructure_hyps =
let destructure_goal =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- Tacmach.New.of_old decidability >>= fun decidability ->
+ let decidability = Tacmach.New.of_old decidability gl in
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 89d161f73..532a2f11d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -454,8 +454,8 @@ let quote_terms ivs lc =
let quote f lid =
Proofview.Goal.enter begin fun gl ->
- Tacmach.New.pf_global f >>= fun f ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+ let f = Tacmach.New.pf_global f gl in
+ let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
let concl = Proofview.Goal.concl gl in
Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
@@ -469,8 +469,9 @@ let quote f lid =
end
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.enter begin fun gl ->
+ let f = Tacmach.New.pf_global f gl in
+ let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
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
@@ -480,6 +481,7 @@ let gen_quote cont c f lid =
match ivs.variable_lhs with
| None -> cont (mkApp (f, [| p |]))
| Some _ -> cont (mkApp (f, [| vm; p |]))
+ end
(*i
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7874f5ac6..f852995a0 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -85,10 +85,12 @@ 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' ->
- Proofview.tclTHEN
- (Proofview.V82.tactic (clenv_refine false clenv'))
- (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
+ Proofview.Goal.enter begin fun gl ->
+ let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in
+ Proofview.tclTHEN
+ (Proofview.V82.tactic (clenv_refine false clenv'))
+ (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
+ end
let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
diff --git a/proofs/goal.ml b/proofs/goal.ml
index fec2503a9..2e7ee10bc 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -354,8 +354,8 @@ let env env _ _ _ = env
let defs _ rdefs _ _ =
!rdefs
-let enter f = (); fun env rdefs _ info ->
- f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info)
+let enter f = (); fun env rdefs gl info ->
+ f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info) gl
(*** Conversion in goals ***)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a19e0d69..fb6c9ddb1 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -149,7 +149,7 @@ val defs : Evd.evar_map sensitive
(* [enter] combines [env], [defs], [hyps] and [concl] in a single
primitive. *)
-val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a) -> 'a sensitive
+val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive
(*** Additional functions ***)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 364cfeb4b..1e0cc7c24 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -668,12 +668,18 @@ end
module Goal = struct
- type t = Environ.env*Evd.evar_map*Environ.named_context_val*Term.constr
-
- let env (env,_,_,_) = env
- let sigma (_,sigma,_,_) = sigma
- let hyps (_,_,hyps,_) = hyps
- let concl (_,_,_,concl) = concl
+ type t = {
+ env : Environ.env;
+ sigma : Evd.evar_map;
+ hyps : Environ.named_context_val;
+ concl : Term.constr ;
+ self : Goal.goal ; (* for compatibility with old-style definitions *)
+ }
+
+ let env { env=env } = env
+ let sigma { sigma=sigma } = sigma
+ let hyps { hyps=hyps } = hyps
+ let concl { concl=concl } = concl
let lift s =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -694,7 +700,9 @@ module Goal = struct
let return x = lift (Goal.return x)
- let enter_t f = Goal.enter (fun env sigma hyps concl -> f (env,sigma,hyps,concl))
+ let enter_t f = Goal.enter begin fun env sigma hyps concl self ->
+ f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
+ end
let enter f =
lift (enter_t f) >= fun ts ->
tclDISPATCH ts
@@ -702,7 +710,11 @@ module Goal = struct
lift (enter_t f) >= fun ts ->
tclDISPATCHL ts >= fun res ->
tclUNIT (List.flatten res)
-
+
+
+ (* compatibility *)
+ let goal { self=self } = self
+
end
module NonLogical = Proofview_monad.NonLogical
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6d5e9d75d..5051e195a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -293,13 +293,15 @@ module Goal : sig
(* [lift_sensitive s] returns the list corresponding to the evaluation
of [s] on each of the focused goals *)
val lift : 'a Goal.sensitive -> 'a glist tactic
-
(* [lift (Goal.return x)] *)
val return : 'a -> 'a glist tactic
val enter : (t -> unit tactic) -> unit tactic
val enterl : (t -> 'a glist tactic) -> 'a glist tactic
+
+ (* compatibility: avoid if possible *)
+ val goal : t -> Goal.goal
end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a50c06b39..8e3ab5975 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -207,65 +207,46 @@ let pr_glls glls =
module New = struct
open Proofview.Notations
- let pf_apply f =
- Proofview.Goal.lift begin
- Goal.env >- fun env ->
- Goal.defs >- fun sigma ->
- Goal.return (f env sigma)
- end
-
- let of_old f =
- Proofview.Goal.lift (Goal.V82.to_sensitive f)
-
- let pf_global_sensitive id =
- Goal.hyps >- fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- Goal.return (Constrintern.construct_reference hyps id)
+ let pf_apply f gl =
+ f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+
+ let of_old f gl =
+ f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
- let pf_global id =
- Proofview.Goal.lift (pf_global_sensitive id)
+ let pf_global id gl =
+ let hyps = Proofview.Goal.hyps gl in
+ let hyps = Environ.named_context_of_val hyps in
+ Constrintern.construct_reference hyps id
- let pf_ids_of_hyps_sensitive =
- Goal.hyps >- fun hyps ->
+ let pf_ids_of_hyps gl =
+ let hyps = Proofview.Goal.hyps gl in
let hyps = Environ.named_context_of_val hyps in
- Goal.return (ids_of_named_context hyps)
- let pf_ids_of_hyps =
- Proofview.Goal.lift pf_ids_of_hyps_sensitive
-
- let pf_get_new_id id =
- Proofview.Goal.lift begin
- pf_ids_of_hyps_sensitive >- fun ids ->
- Goal.return (next_ident_away id ids)
- end
-
- let pf_get_hyp_sensitive id =
- Goal.hyps >- fun hyps ->
+ ids_of_named_context hyps
+
+ let pf_get_new_id id gl =
+ let ids = pf_ids_of_hyps gl in
+ next_ident_away id ids
+
+ let pf_get_hyp id gl =
+ let hyps = Proofview.Goal.hyps gl in
let hyps = Environ.named_context_of_val hyps in
let sign =
try Context.lookup_named id hyps
with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
in
- Goal.return sign
- let pf_get_hyp id =
- Proofview.Goal.lift (pf_get_hyp_sensitive id)
-
- let pf_get_hyp_typ_sensitive id =
- pf_get_hyp_sensitive id >- fun (_,_,ty) ->
- Goal.return ty
- let pf_get_hyp_typ id =
- Proofview.Goal.lift (pf_get_hyp_typ_sensitive id)
-
- let pf_hyps_types =
- Proofview.Goal.lift begin
- Goal.env >- fun env ->
- let sign = Environ.named_context env in
- Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
- end
-
- let pf_last_hyp =
- Proofview.Goal.lift begin
- Goal.hyps >- fun hyps ->
- Goal.return (List.hd (Environ.named_context_of_val hyps))
- end
+ sign
+
+ let pf_get_hyp_typ id gl =
+ let (_,_,ty) = pf_get_hyp id gl in
+ ty
+
+ let pf_hyps_types gl =
+ let env = Proofview.Goal.env gl in
+ let sign = Environ.named_context env in
+ List.map (fun (id,_,x) -> (id, x)) sign
+
+ let pf_last_hyp gl =
+ let hyps = Proofview.Goal.hyps gl in
+ List.hd (Environ.named_context_of_val hyps)
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7c96bd93b..1ca15d9ae 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,31 +134,17 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
- open Goal
open Proofview
- val pf_apply : (env -> evar_map -> 'a) -> 'a glist tactic
- val pf_global_sensitive : identifier -> constr sensitive
- val pf_global : identifier -> constr glist tactic
- val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a glist tactic
-
- val pf_get_new_id : identifier -> identifier glist tactic
- val pf_ids_of_hyps_sensitive : identifier list sensitive
- val pf_ids_of_hyps : identifier list glist tactic
- val pf_hyps_types : (identifier * types) list glist tactic
-
- val pf_get_hyp_sensitive : identifier -> named_declaration sensitive
- val pf_get_hyp : identifier -> named_declaration glist tactic
- val pf_get_hyp_typ_sensitive : identifier -> types sensitive
- val pf_get_hyp_typ : identifier -> types glist tactic
- val pf_last_hyp : named_declaration glist tactic
-end
-
-
-
-
-
-
-
+ val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
+ val pf_global : identifier -> Proofview.Goal.t -> constr
+ val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
+ val pf_get_new_id : identifier -> Proofview.Goal.t -> identifier
+ val pf_ids_of_hyps : Proofview.Goal.t -> identifier list
+ val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list
+ val pf_get_hyp : identifier -> Proofview.Goal.t -> named_declaration
+ val pf_get_hyp_typ : identifier -> Proofview.Goal.t -> types
+ val pf_last_hyp : Proofview.Goal.t -> named_declaration
+end
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 728eaa3fe..29381c7c8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1278,7 +1278,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
( Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
- Tacmach.New.pf_last_hyp >>= fun hyp ->
+ let hyp = Tacmach.New.pf_last_hyp gl in
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
end)
@@ -1376,20 +1376,24 @@ let make_db_list dbnames =
List.map lookup dbnames
let trivial ?(debug=Off) lems dbnames =
+ Proofview.Goal.enter begin fun gl ->
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 ->
+ let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
new_tclTRY_dbg d
(trivial_fail_db d false db_list hints)
+ end
let full_trivial ?(debug=Off) lems =
+ Proofview.Goal.enter begin fun gl ->
let dbs = !searchtable in
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 ->
+ let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
new_tclTRY_dbg d
(trivial_fail_db d false db_list hints)
+ end
let gen_trivial ?(debug=Off) lems = function
| None -> full_trivial ~debug lems
@@ -1423,8 +1427,10 @@ 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 ->
- Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)))
+ (Proofview.Goal.enter begin fun gl ->
+ let extend_local_db = Tacmach.New.of_old extend_local_db gl in
+ Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
+ end)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
@@ -1452,12 +1458,13 @@ let search d n mod_delta db_list local_db =
let default_search_depth = ref 5
let delta_auto ?(debug=Off) mod_delta n lems dbnames =
- Proofview.tclUNIT () >= fun () -> (* delay for the side effects *)
+ Proofview.Goal.enter begin fun gl ->
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 ->
+ let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
new_tclTRY_dbg d
(search d n mod_delta db_list hints)
+ end
let auto ?(debug=Off) n = delta_auto ~debug false n
@@ -1466,13 +1473,15 @@ let new_auto ?(debug=Off) n = delta_auto ~debug true n
let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
+ Proofview.Goal.enter begin fun gl ->
let dbs = !searchtable in
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 ->
+ let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
new_tclTRY_dbg d
(search d n mod_delta db_list hints)
+ end
let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 9c1f462ba..da8f2668b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -113,8 +113,9 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(Proofview.tclUNIT()) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
+ Proofview.Goal.enter begin fun gl ->
(* 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 _ ->
+ let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
let general_rewrite_in id =
let id = ref id in
let to_be_cleared = ref false in
@@ -155,6 +156,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
(List.fold_left (fun tac bas ->
Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas)))
idl
+ end
let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
@@ -179,8 +181,10 @@ 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 ->
- try_do_hyps (fun id -> id) ids)
+ Proofview.Goal.enter begin fun gl ->
+ let ids = Tacmach.New.pf_ids_of_hyps gl in
+ try_do_hyps (fun id -> id) ids
+ end)
let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT())
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c500a5969..5a244fe7d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -62,11 +62,11 @@ let contradiction_context =
else match kind_of_term typ with
| Prod (na,t,u) when is_empty_type u ->
(Proofview.tclORELSE
- begin
- Tacmach.New.pf_apply is_conv_leq >>= fun is_conv_leq ->
+ (Proofview.Goal.enter begin fun gl ->
+ let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
filter_hyp (fun typ -> is_conv_leq typ t)
(fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
- end
+ end)
begin function
| Not_found -> seek_neg rest
| e -> Proofview.tclZERO e
@@ -87,7 +87,7 @@ let contradiction_term (c,lbind as cl) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
try (* type_of can raise exceptions. *)
let typ = type_of c in
let _, ccl = splay_prod env sigma typ in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b9f077aa4..de4c58371 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -86,7 +86,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
try (* type_of can raise exceptions *)
let typc = type_of c in
Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
@@ -96,6 +97,7 @@ let general_decompose recognizer c =
(fun id -> Proofview.V82.tactic (clear [id]))));
Proofview.V82.tactic (exact_no_check c) ]
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let head_in =
Goal.env >- fun env ->
@@ -169,8 +171,9 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let abs_i = Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) gl in
+ let abs_j = Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) gl in
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
@@ -182,6 +185,7 @@ let double_ind h1 h2 =
Tacticals.New.elimination_then
(introElimAssumsThen (induction_trailer abs_i abs_j))
([],[]) (mkVar id))))
+ end
let h_double_induction = double_ind
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index a0e8fcb88..ee398a8b4 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -120,12 +120,16 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let rectype = Tacmach.New.of_old (fun g -> pf_type_of g a1) gl in
+ let decide =
+ Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) gl
+ in
let subtacs =
if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
else [diseqCase eqonleft;eqCase tac;default_auto] in
(Tacticals.New.tclTHENS (Proofview.V82.tactic (h_elim_type decide)) subtacs)
+ end
let solveEqBranch rectype =
Proofview.tclORELSE
@@ -160,7 +164,7 @@ let decideGralEquality =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
- Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
+ let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in
begin match kind_of_term headtyp with
| Ind mi -> Proofview.tclUNIT mi
| _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
@@ -179,20 +183,24 @@ let decideGralEquality =
let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality
let decideEquality rectype =
- Tacmach.New.of_old (mkGenDecideEqGoal rectype) >>= fun decide ->
+ Proofview.Goal.enter begin fun gl ->
+ let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in
(Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide)) [default_auto;decideEqualityGoal])
+ end
(* 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in
+ let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in
(Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide))
[(Tacticals.New.tclTHEN intro
(Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case)
(Proofview.V82.tactic clear_last)));
decideEquality rectype])
+ end
(* User syntax *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 782ca67d5..284199586 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -221,17 +221,18 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
| Some (tac, FirstSolved) -> true, true, Some (Tacticals.New.tclCOMPLETE tac)
| Some (tac, AllMatches) -> true, false, Some (Tacticals.New.tclCOMPLETE tac)
in
- let cs =
- Goal.env >- fun env ->
- Goal.concl >- fun concl ->
- Goal.V82.to_sensitive (
- (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
- env ) >- fun instantiate_lemma ->
- let typ =
- match cls with None -> Goal.return concl | Some id -> Tacmach.New.pf_get_hyp_typ_sensitive id
- in
- typ >- fun typ ->
- Goal.return (instantiate_lemma c t l l2r typ)
+ let cs gl =
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ let instantiate_lemma =
+ Tacmach.New.of_old
+ ((if not all then instantiate_lemma else instantiate_lemma_all frzevars) env)
+ gl
+ in
+ let typ =
+ match cls with None -> concl | Some id -> Tacmach.New.pf_get_hyp_typ id gl
+ in
+ instantiate_lemma c t l l2r typ
in
let try_clause c =
side_tac
@@ -240,11 +241,13 @@ 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.enter begin fun gl ->
+ let cs = cs gl in
if firstonly then
Tacticals.New.tclFIRST (List.map try_clause cs)
else
Tacticals.New.tclMAP try_clause cs
+ end
(* The next function decides in particular whether to try a regular
rewrite or a generalized rewrite.
@@ -325,18 +328,22 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
let type_of_clause = function
| None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl))
- | Some id -> Tacmach.New.pf_get_hyp_typ id
+ | Some id -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Tacmach.New.pf_get_hyp_typ id gl))
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
+ Proofview.Goal.enter begin fun gl ->
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 ->
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) ->
+ let (elim,effs) =
+ Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) gl
+ in
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)
{elimindex = None; elimbody = (elim,NoBindings)}
+ end
let adjust_rewriting_direction args lft2rgt =
match args with
@@ -449,13 +456,14 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
in
let do_hyps =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
- let ids =
+ let ids gl =
let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
- 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)
+ let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
+ 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 ->
- do_hyps_atleastonce ids
+ Proofview.Goal.enter begin fun gl ->
+ do_hyps_atleastonce (ids gl)
+ end
in
if cl.concl_occs == NoOccurrences then do_hyps else
Tacticals.New.tclIFTHENTRYELSEMUST
@@ -508,10 +516,11 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let get_type_of = Tacmach.New.pf_apply get_type_of gl in
let t1 = get_type_of c1
and t2 = get_type_of c2 in
- Tacmach.New.pf_apply is_conv >>= fun is_conv ->
+ let is_conv = Tacmach.New.pf_apply is_conv gl in
if unsafe || (is_conv t1 t2) then
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
@@ -529,7 +538,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
]
else
Tacticals.New.tclFAIL 0 (str"Terms do not have convertible types.")
-
+ end
let replace c2 c1 = multi_replace onConcl c2 c1 false None
@@ -794,12 +803,14 @@ let rec build_discriminator sigma env dirn c sort = function
*)
let gen_absurdity id =
- Tacmach.New.pf_get_hyp_typ id >>= fun hyp_typ ->
+ Proofview.Goal.enter begin fun gl ->
+ let hyp_typ = Tacmach.New.pf_get_hyp_typ id gl in
if is_empty_type hyp_typ
then
simplest_elim (mkVar id)
else
Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+ end
(* Precondition: eq is leibniz equality
@@ -860,28 +871,31 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
| 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 ->
- let sort = get_type_of concl in
+ let sort = Tacmach.New.pf_apply get_type_of gl concl in
discr_positions env sigma u eq_clause cpath dirn sort
end
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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+ let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in
try (* type_of can raise exceptions *)
let t = type_of c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
- Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) >>= fun eq_clause ->
+ let eq_clause = Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) gl in
begin try (* clenv_pose_dependent_evars can raise exceptions *)
let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
let eqn = clenv_type eq_clause' in
- Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) >>= fun (eq,eq_args) ->
+ let (eq,eq_args) =
+ Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) gl
+ in
Tacticals.New.tclTHEN
(Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
(tac (eq,eqn,eq_args) eq_clause')
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let onNegatedEquality with_evars tac =
Proofview.Goal.enter begin fun gl ->
@@ -1278,7 +1292,9 @@ let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
- Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
+ let sort =
+ Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) gl
+ in
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
match find_positions env sigma t1 t2 with
@@ -1572,7 +1588,7 @@ let subst_one_var dep_proof_ok x =
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let hyps = Environ.named_context_of_val hyps in
- Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
+ let (_,xval,_) = Tacmach.New.pf_get_hyp x gl in
(* 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: *)
@@ -1586,7 +1602,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) ->
+ let (hyp,rhs,dir) = Tacmach.New.of_old found gl in
subst_one dep_proof_ok x (hyp,rhs,dir)
end
@@ -1611,7 +1627,8 @@ let default_subst_tactic_flags () =
{ only_leibniz = true; rewrite_dependent_proof = false }
let subst_all ?(flags=default_subst_tactic_flags ()) () =
- Tacmach.New.of_old find_eq_data_decompose >>= fun find_eq_data_decompose ->
+ Proofview.Goal.enter begin fun gl ->
+ let find_eq_data_decompose = Tacmach.New.of_old find_eq_data_decompose gl in
let test (_,c) =
try
let lbeq,(_,x,y) = find_eq_data_decompose c in
@@ -1623,10 +1640,11 @@ 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 ->
+ let hyps = Tacmach.New.pf_hyps_types gl in
let ids = List.map_filter test hyps in
let ids = List.uniquize ids in
subst_gen flags.rewrite_dependent_proof ids
+ end
(* Rewrite the first assumption for which the condition faildir does not fail
and gives the direction of the rewrite *)
@@ -1679,6 +1697,9 @@ let replace_multi_term dir_opt c =
| Some true -> cond_eq_term_left c
| Some false -> cond_eq_term_right c
in
+ let cond_eq_fun t =
+ Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (cond_eq_fun t gl))
+ in
rewrite_multi_assumption_cond cond_eq_fun
let _ =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fcb131161..088ce71d4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -644,10 +644,12 @@ END
exception Found of unit Proofview.tactic
let rewrite_except h =
- Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
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
+ end
let refl_equal =
@@ -661,7 +663,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
Proofview.Goal.enter begin fun gl ->
@@ -673,6 +676,7 @@ let mkCaseEq a : unit Proofview.tactic =
end
end;
simplest_case a]
+ end
let case_eq_intros_rewrite x =
@@ -685,9 +689,9 @@ let case_eq_intros_rewrite x =
mkCaseEq x;
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
let n' = nb_prod concl in
- Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h ->
+ let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
Tacticals.New.tclTHENLIST [
Tacticals.New.tclDO (n'-n-1) intro;
Proofview.V82.tactic (Tacmach.introduction h);
@@ -713,10 +717,12 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
+ end
TACTIC EXTEND destauto
| [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b3c8b2837..ebccd95b7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -274,11 +274,13 @@ Nota: with Inversion_clear, only four useless hypotheses
*)
let generalizeRewriteIntros tac depids id =
- Tacmach.New.of_old (dependent_hyps id depids) >>= fun dids ->
+ Proofview.Goal.enter begin fun gl ->
+ let dids = Tacmach.New.of_old (dependent_hyps id depids) gl in
(Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (bring_hyps dids); tac;
(* may actually fail to replace if dependent in a previous eq *)
intros_replacing (ids_of_named_context dids)])
+ end
let rec tclMAP_i n tacfun = function
| [] -> Tacticals.New.tclDO n (tacfun None)
@@ -302,11 +304,15 @@ 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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (t,t1,t2) =
+ Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) gl
+ in
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
| _ -> tac id
+ end
in
let deq_trailer id _ neqns =
Tacticals.New.tclTHENLIST
@@ -331,7 +337,10 @@ 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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (depids,nodepids) =
+ Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) gl
+ in
let rewrite_eqns =
match othin with
| Some thin ->
@@ -361,6 +370,7 @@ let rewrite_equations_gene othin neqns ba =
(tclORELSE (clear [id])
(tclTHEN (bring_hyps [d]) (clear [id]))))
depids)])
+ end
(* Introduction of the equations on arguments
othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -397,8 +407,11 @@ let extract_eqn_names = function
| Some x -> x
let rewrite_equations othin neqns names ba =
+ Proofview.Goal.enter begin fun gl ->
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) ->
+ let (depids,nodepids) =
+ Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) gl
+ in
let rewrite_eqns =
let first_eq = ref MoveLast in
match othin with
@@ -424,6 +437,7 @@ let rewrite_equations othin neqns names ba =
Proofview.V82.tactic (bring_hyps nodepids);
Proofview.V82.tactic (clear (ids_of_named_context nodepids));
rewrite_eqns])
+ end
let interp_inversion_kind = function
| SimpleInversion -> None
@@ -448,8 +462,8 @@ let raw_inversion inv_kind id status names =
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
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 ->
+ let reduce_to_atomic_ind = Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind gl in
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
begin
try
Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
@@ -457,7 +471,7 @@ let raw_inversion inv_kind id status names =
Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
str ("The type of "^(Id.to_string id)^" is not inductive.")))
end >= fun (ind,t) ->
- Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
+ let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in
let ccl = clenv_type indclause in
check_no_metas indclause ccl;
let IndType (indf,realargs) = find_rectype env sigma ccl in
@@ -526,7 +540,7 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
let invIn k names ids id =
Proofview.Goal.enter begin fun gl ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+ let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
let concl = Proofview.Goal.concl gl in
let nb_prod_init = nb_prod concl in
let intros_replace_ids =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e726e7692..86ec3a835 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -285,7 +285,7 @@ let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv i
let lemInvIn id c ids =
Proofview.Goal.enter begin fun gl ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+ let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
let intros_replace_ids =
let concl = Proofview.Goal.concl gl in
let nb_of_new_hyp = nb_prod concl - List.length ids in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 14a9eb0ed..f40ec7659 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1820,7 +1820,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let ctype = Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) gl in
let binders,concl = decompose_prod_assum ctype in
let (equiv, args) = decompose_app concl in
let rec split_last_two = function
@@ -1835,6 +1836,7 @@ let setoid_symmetry_in id =
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) ] ]
+ end
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 83958eca2..2bf3c8e06 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1179,9 +1179,11 @@ 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) ->
- Proofview.V82.tclEVARS sigma <*>
- (Proofview.Goal.return v)
+ Proofview.Goal.enterl begin fun gl ->
+ let (sigma,v) = Tacmach.New.of_old f gl in
+ Proofview.V82.tclEVARS sigma <*>
+ (Proofview.Goal.return v)
+ end
in
match arg with
| TacGeneric arg ->
@@ -1209,8 +1211,10 @@ 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 ->
+ Proofview.Goal.enterl begin fun gl ->
+ let id = Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) gl in
(Proofview.Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)))
+ end
| Tacexp t -> val_interp ist t
| TacDynamic(_,t) ->
let tg = (Dyn.tag t) in
@@ -1465,8 +1469,8 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
end
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
+ apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) gl in
+ match_next_pattern init_match_pattern
| [] ->
let lfun = lfun +++ ist.lfun in
let lfun = extend_values_with_bindings lmatch lfun in
@@ -1712,8 +1716,12 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let patterns =
+ Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) gl
+ in
h_intro_patterns patterns
+ end
| TacIntrosUntil hyp ->
begin try (* interp_quantified_hypothesis can raise an exception *)
h_intros_until (interp_quantified_hypothesis ist hyp)
@@ -1722,7 +1730,7 @@ and interp_atomic ist tac =
| TacIntroMove (ido,hto) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
+ let mloc = Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) gl in
h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
end
| TacAssumption -> Proofview.V82.tactic h_assumption
@@ -1762,8 +1770,10 @@ 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 ->
- h_apply_in a ev l cl) in
+ Proofview.Goal.enter begin fun gl ->
+ let cl = Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) gl in
+ h_apply_in a ev l cl
+ end) in
Tacticals.New.tclWITHHOLES ev tac sigma l
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
@@ -1858,7 +1868,7 @@ and interp_atomic ist tac =
let sigma = Proofview.Goal.sigma gl in
try (* intrerpreation function may raise exceptions *)
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 ->
+ let patt = Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) gl in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(Tactics.forward (Option.map (interp_tactic ist) t)
@@ -1884,11 +1894,15 @@ and interp_atomic ist tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- 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 ->
+ let clp = Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) gl in
+ let eqpat =
+ Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) gl
+ in
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) ->
+ let (sigma,c_interp) =
+ Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+ in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
@@ -1926,21 +1940,20 @@ and interp_atomic ist tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
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 ->
- Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
- Goal.return begin
- c,
- (Option.map interp_intro_pattern ipato,
- Option.map interp_intro_pattern ipats)
- end
+ List.map begin fun (c,(ipato,ipats)) ->
+ let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in
+ let interp_intro_pattern =
+ Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) gl
+ in
+ c,
+ (Option.map interp_intro_pattern ipato,
+ Option.map interp_intro_pattern ipats)
end l
in
let sigma = Proofview.Goal.sigma gl in
- 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 ->
+ let interp_clause = Tacmach.New.of_old (fun gl -> interp_clause ist gl) gl in
let cls = Option.map interp_clause cls in
Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
end
@@ -1949,21 +1962,27 @@ 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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(Elim.h_decompose_and c_interp)
+ end
| TacDecomposeOr c ->
- Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(Elim.h_decompose_or c_interp)
+ end
| TacDecompose (l,c) ->
+ Proofview.Goal.enter begin fun gl ->
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) ->
+ let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(Elim.h_decompose l c_interp)
+ end
| TacSpecialize (n,cb) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -2095,71 +2114,94 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let cl = Tacmach.New.of_old (fun gl -> interp_clause ist gl c) gl in
h_symmetry cl
+ end
| 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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (sigma,c_interp) =
+ Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+ in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARS sigma)
(h_transitivity (Some c_interp))
+ end
end
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
+ Proofview.Goal.enter begin fun gl ->
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 ->
+ let cl = Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) gl in
Equality.general_multi_multi_rewrite ev l cl
(Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)
+ end
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.lift begin match c with
- | None -> Goal.return (sigma , None)
- | 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let (sigma,c_interp) =
+ match c with
+ | None -> sigma , None
+ | Some c ->
+ let (sigma,c_interp) =
+ Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+ in
+ sigma , Some c_interp
+ in
+ let interp_intro_pattern = Tacmach.New.of_old (interp_intro_pattern ist) gl in
+ let dqhyps =
+ Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl
+ in
Inv.dinv k c_interp
(Option.map interp_intro_pattern ids)
dqhyps
+ end
| 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let interp_intro_pattern = Tacmach.New.of_old (interp_intro_pattern ist) gl in
+ let hyps = Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) gl in
+ let dqhyps = Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl in
Inv.inv_clause k
(Option.map interp_intro_pattern ids)
hyps
dqhyps
+ end
| 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
+ let dqhyps = Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl in
+ let hyps = Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) gl in
Leminv.lemInv_clause dqhyps
c_interp
hyps
+ end
(* For extensions *)
| TacExtend (loc,opn,l) ->
- Proofview.tclEVARMAP >= fun goal_sigma ->
+ Proofview.Goal.enter begin fun gl ->
+ let goal_sigma = Proofview.Goal.sigma gl in
let tac = lookup_tactic opn in
- Tacmach.New.of_old begin fun gl ->
+ let (sigma,args) = Tacmach.New.of_old begin fun gl ->
List.fold_right begin fun a (sigma,acc) ->
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 gl in
Proofview.V82.tclEVARS sigma <*>
tac args ist
+ end
| TacAlias (loc,s,l,(_,body)) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let rec f x = match genarg_tag x with
+ let rec f x =
+ Proofview.Goal.enterl begin fun gl ->
+ match genarg_tag x with
| IntOrVarArgType ->
(Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
| IdentArgType b ->
@@ -2168,40 +2210,49 @@ and interp_atomic ist tac =
(out_gen (glbwit (wit_ident_gen b)) x)))
end
| VarArgType ->
- Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))
+ Proofview.Goal.return (
+ Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))
+ gl
+ )
| RefArgType ->
+ Proofview.Goal.return (
Tacmach.New.of_old (fun gl ->
Value.of_constr (constr_of_global
(pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
+ gl
+ )
| 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) ->
+ Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
(Proofview.V82.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) ->
+ Proofview.Goal.return (
+ Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
(Proofview.V82.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) ->
+ Proofview.Goal.return (
+ Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x))
+ gl) >>== fun (sigma,c_interp) ->
Proofview.V82.tclEVARS sigma <*>
Proofview.Goal.return (Value.of_constr c_interp)
| ListArgType ConstrArgType ->
let wit = glbwit (wit_list wit_constr) in
- Tacmach.New.of_old begin fun gl ->
+ let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
List.fold_right begin fun c (sigma,acc) ->
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 gl in
(Proofview.V82.tclEVARS sigma) <*>
(Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
| ListArgType VarArgType ->
let wit = glbwit (wit_list wit_var) in
- Tacmach.New.of_old (fun gl ->
+ Proofview.Goal.return (Tacmach.New.of_old (fun gl ->
let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
in_gen (topwit (wit_list wit_genarg)) ans
- )
+ ) gl)
| ListArgType IntOrVarArgType ->
let wit = glbwit (wit_list wit_int_or_var) in
let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
@@ -2228,8 +2279,8 @@ and interp_atomic ist tac =
val_interp ist tac >>== fun v ->
Proofview.Goal.return v
else
- Tacmach.New.of_old (fun gl ->
- Geninterp.generic_interp ist gl x) >>== fun (newsigma,v) ->
+ let (newsigma,v) = Tacmach.New.of_old (fun gl ->
+ Geninterp.generic_interp ist gl x) gl in
Proofview.V82.tactic (tclEVARS newsigma) <*>
Proofview.Goal.return v
| QuantHypArgType | RedExprArgType
@@ -2237,6 +2288,7 @@ and interp_atomic ist tac =
| BindingsArgType
| OptArgType _ | PairArgType _
-> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations."))
+ end
in
let addvar (x, v) accu =
accu >>== fun accu ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5d3c8b97a..265af5b08 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -554,38 +554,47 @@ module New = struct
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Tacmach.New.pf_get_hyp_typ id >>= fun typ ->
+ Proofview.Goal.enter begin fun gl ->
+ let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
else
tac2 id
+ end
let fullGoal =
- Tacmach.New.pf_ids_of_hyps >>== fun hyps ->
+ Proofview.Goal.enterl begin fun gl ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
Proofview.Goal.return (None :: List.map Option.make hyps)
+ end
let tryAllHyps tac =
- Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclFIRST_PROGRESS_ON tac hyps
+ end
let tryAllHypsAndConcl tac =
fullGoal >>= fun fullGoal ->
tclFIRST_PROGRESS_ON tac fullGoal
let onClause tac cl =
- Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
+ end
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
isrec allnames tac predicate (indbindings,elimbindings)
ind indclause =
- Tacmach.New.of_old (mk_elim ind) >>= fun elim ->
+ Proofview.Goal.enter begin fun gl ->
+ let elim = Tacmach.New.of_old (mk_elim ind) gl in
(* 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 ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
begin try (* type_of can raise an exception *)
- Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim))
+ Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) gl)
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end >>= fun elimclause ->
let indmv =
@@ -634,10 +643,14 @@ module New = struct
Reduction.CONV (mkMeta pmv) p elimclause'
in
new_elim_res_pf_THEN_i elimclause' branchtacs
+ end
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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let (ind,t) =
+ Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
+ in
+ let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in
let isrec,mkelim =
if (Global.lookup_mind (fst ind)).mind_record
then false,gl_make_case_dep
@@ -645,6 +658,7 @@ module New = struct
in
general_elim_then_using mkelim isrec
None tac predicate bindings ind indclause
+ end
let case_then_using =
general_elim_then_using gl_make_case_dep false
@@ -656,10 +670,14 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
tac branches
+ end
let case_on_ba tac ba =
- Tacmach.New.of_old (make_case_branch_assumptions ba) >>= fun branches ->
+ Proofview.Goal.enter begin fun gl ->
+ let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
tac branches
+ end
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e62451f9..c317ca0d4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -606,8 +606,10 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in
Tacticals.New.tclDO n (if red then introf else intro)
+ end
let intros_until_id id = intros_until_gen true (NamedHyp id)
let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
@@ -873,8 +875,10 @@ let find_eliminator c gl =
let default_elim with_evars (c,_ as cx) =
Proofview.tclORELSE
- (Tacmach.New.of_old (find_eliminator c) >>= fun elim ->
- Proofview.V82.tactic (general_elim with_evars cx elim))
+ (Proofview.Goal.enter begin fun gl ->
+ let elim = Tacmach.New.of_old (find_eliminator c) gl in
+ Proofview.V82.tactic (general_elim with_evars cx elim)
+ end)
begin function
| IsRecord ->
(* For records, induction principles aren't there by default
@@ -1285,7 +1289,9 @@ let check_number_of_constructors expctdnumopt i nconstr =
let constructor_tac with_evars expctdnumopt i lbind =
Proofview.Goal.enter begin fun gl ->
let cl = Proofview.Goal.concl gl in
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+ let reduce_to_quantified_ind =
+ Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
+ in
try (* reduce_to_quantified_ind can raise an exception *)
let (mind,redcl) = reduce_to_quantified_ind cl in
let nconstr =
@@ -1309,7 +1315,9 @@ let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
Proofview.Goal.enter begin fun gl ->
let cl = Proofview.Goal.concl gl in
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+ let reduce_to_quantified_ind =
+ Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
+ in
try (* reduce_to_quantified_ind can raise an exception *)
let mind = fst (reduce_to_quantified_ind cl) in
let nconstr =
@@ -1386,9 +1394,12 @@ let intro_decomp_eq loc b l l' thin tac id gl =
(eq,t,eq_args) eq_clause) gl
let intro_or_and_pattern loc b ll l' thin tac id =
+ Proofview.Goal.enter begin fun gl ->
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) ->
+ let (ind,t) =
+ Tacmach.New.of_old (fun gl ->
+ pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
+ in
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
@@ -1398,6 +1409,7 @@ let intro_or_and_pattern loc b ll l' thin tac id =
(Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
(Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
nv (Array.of_list ll))
+ end
let rewrite_hyp l2r id =
let rew_on l2r =
@@ -1408,8 +1420,8 @@ let rewrite_hyp l2r id =
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
- Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+ let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
try (* type_of can raise an exception *)
let t = whd_betadeltaiota (type_of (mkVar id)) in
(* TODO: detect setoid equality? better detect the different equalities *)
@@ -1518,41 +1530,32 @@ let intro_patterns = function
let make_id s = fresh_id [] (default_id_of_sort s)
-let prepare_intros s ipat =
- let make_id s = Tacmach.New.of_old (make_id s) in
- let fresh_id l id = Tacmach.New.of_old (fresh_id l id) in
- let (>>=) t k =
- t >>== fun x ->
- Proofview.Goal.return (k x)
- in
+let prepare_intros s ipat gl =
+ let make_id s = Tacmach.New.of_old (make_id s) gl in
+ let fresh_id l id = Tacmach.New.of_old (fresh_id l id) gl in
match ipat with
| None ->
- make_id s >>= fun id ->
- id , Proofview.tclUNIT ()
+ make_id s , Proofview.tclUNIT ()
| Some (loc,ipat) -> match ipat with
| IntroIdentifier id ->
- Proofview.Goal.return (id, Proofview.tclUNIT ())
+ id, Proofview.tclUNIT ()
| IntroAnonymous ->
- make_id s >>= fun id ->
- id , Proofview.tclUNIT ()
+ make_id s , Proofview.tclUNIT ()
| IntroFresh id ->
- fresh_id [] id >>= fun id ->
- id , Proofview.tclUNIT ()
+ fresh_id [] id , Proofview.tclUNIT ()
| IntroWildcard ->
- make_id s >>= fun id ->
+ let id = make_id s in
id , Proofview.V82.tactic (clear_wildcards [dloc,id])
| IntroRewrite l2r ->
- make_id s >>= fun id ->
- id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+ let id = make_id s in
+ id , Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
| IntroOrAndPattern ll ->
- make_id s >>= fun id ->
- id ,
+ make_id s ,
Tacticals.New.onLastHypId
(intro_or_and_pattern loc true ll [] []
(fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
| IntroInjection l ->
- make_id s >>= fun id ->
- id ,
+ make_id s ,
Proofview.V82.tactic (onLastHypId
(intro_decomp_eq loc true l [] []
(fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
@@ -1577,15 +1580,17 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let hnf_type_of = Tacmach.New.of_old pf_hnf_type_of gl in
match kind_of_term (hnf_type_of c) with
| Sort s ->
- prepare_intros s ipat >>= fun (id,tac) ->
+ let (id,tac) = prepare_intros s ipat gl in
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))
(if first then [Proofview.tclUNIT (); tac] else [tac; Proofview.tclUNIT ()])
| _ -> Proofview.tclZERO (Errors.UserError ("",str"Not a proposition or a type."))
+ end
let assert_tac na = assert_as true (ipat_of_name na)
@@ -1908,36 +1913,33 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
let id =
let t = match ty with Some t -> t | None -> typ_of env sigmac c in
let x = id_of_name_using_hdchar (Global.env()) t name in
- if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else
- Proofview.Goal.lift begin
- if not (mem_named_context x hyps) then Goal.return x else
+ if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else
+ if not (mem_named_context x hyps) then 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) ->
- 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 ->
- let newcl = match with_eq with
+ in
+ let (depdecls,lastlhyp,ccl,c) =
+ Tacmach.New.of_old (letin_abstract id c test occs) gl
+ in
+ let t =
+ match ty with Some t -> t | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) gl
+ in
+ let (newcl,eq_tac) = match with_eq with
| Some (lr,(loc,ido)) ->
let heq = match ido with
- | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id))
- | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base)
- | IntroIdentifier id -> (Proofview.Goal.return id)
- | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in
- heq >>== fun heq ->
+ | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) gl
+ | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) gl
+ | IntroIdentifier id -> id
+ | _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let eq = applist (eqdata.eq,args) in
let refl = applist (eqdata.refl, [t;mkVar id]) in
- Proofview.Goal.return begin
mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
Tacticals.New.tclTHEN
(intro_gen loc (IntroMustBe heq) lastlhyp true false)
(Proofview.V82.tactic (thin_body [heq;id]))
- end
| None ->
- (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
- newcl >>= fun (newcl,eq_tac) ->
+ (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
Tacticals.New.tclTHENLIST
[ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
intro_gen dloc (IntroMustBe id) lastlhyp true false;
@@ -1964,12 +1966,14 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
begin try (* type_of can raise an exception *)
let t = type_of c in
Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
+ end
| Some tac ->
Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
@@ -2121,30 +2125,36 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
match ra with
| (RecArg,deprec,recvarname) ::
(IndArg,depind,hyprecname) :: ra' ->
- let recpat = match names with
+ Proofview.Goal.enter begin fun gl ->
+ let (recpat,names) = match names with
| [loc,IntroIdentifier id as pat] ->
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) ->
+ (pat, [dloc, IntroIdentifier id'])
+ | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) gl in
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) ->
- safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
- peel_tac ra' (update_dest dests ids') names thin))
+ Proofview.Goal.enter begin fun gl ->
+ let (hyprec,names) =
+ Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) gl
+ in
+ safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
+ peel_tac ra' (update_dest dests ids') names thin)
+ end)
+ end
| (IndArg,dep,hyprecname) :: ra' ->
+ Proofview.Goal.enter begin fun gl ->
(* 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) ->
+ let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) gl in
safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
+ end
| (RecArg,dep,recvarname) :: ra' ->
- let pat = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) in
- pat >>= fun (pat,names) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) gl in
let dest = get_recarg_dest dests in
safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
+ end
| (OtherArg,_,_) :: ra' ->
let pat,names = match names with
| [] -> (dloc, IntroAnonymous), []
@@ -2165,8 +2175,9 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
+ let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
try (* reduce_to_quantified_ref can raise an exception *)
let typ0 = reduce_to_quantified_ref indref tmptyp0 in
let prods, indtyp = decompose_prod typ0 in
@@ -2176,10 +2187,12 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let rec atomize_one i avoid =
Proofview.Goal.enter begin fun gl ->
if not (Int.equal i nparams) then
- Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
+ let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
(* 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 ->
+ let reduce_to_atomic_ref =
+ Tacmach.New.pf_apply reduce_to_atomic_ref gl
+ in
let indtyp = reduce_to_atomic_ref indref tmptyp0 in
let argl = snd (decompose_app indtyp) in
let c = List.nth argl (i-1) in
@@ -2188,15 +2201,15 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
| 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 ->
+ let x = Tacmach.New.of_old (fresh_id [] id) gl in
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 ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
let id = id_of_name_using_hdchar (Global.env()) (type_of c)
Anonymous in
- Tacmach.New.of_old (fresh_id [] id) >>= fun x ->
+ let x = Tacmach.New.of_old (fresh_id [] id) gl in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
(atomize_one (i-1) ((mkVar x)::avoid))
@@ -2206,6 +2219,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
in
atomize_one (List.length argl) params
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let find_atomic_param_of_ind nparams indtyp =
let argl = snd (decompose_app indtyp) in
@@ -2663,25 +2677,22 @@ let abstract_args gl generalize_vars dep id defined f args =
else None
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
- Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
+ Proofview.Goal.enter begin fun gl ->
Coqlib.check_required_library Coqlib.jmeq_module_name;
- let args =
- Tacmach.New.pf_get_new_id id >>== fun oldid ->
- Tacmach.New.pf_get_hyp id >>== fun (_, b, t) ->
- Proofview.Goal.return begin
+ let (f, args, def, id, oldid) =
+ let oldid = Tacmach.New.pf_get_new_id id gl in
+ let (_, b, t) = Tacmach.New.pf_get_hyp id gl in
match b with
| None -> let f, args = decompose_app t in
(f, args, false, id, oldid)
| Some t ->
let f, args = decompose_app t in
(f, args, true, id, oldid)
- end
in
- args >>= fun (f, args, def, id, oldid) ->
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 ->
+ let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
match newc with
| None -> Proofview.tclUNIT ()
| Some (newc, dep, n, vars) ->
@@ -2697,6 +2708,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
(Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ;
tclMAP (fun id ->
tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl))
+ end
let rec compare_upto_variables x y =
if (isVar x || isRel x) && (isVar y || isRel y) then true
@@ -3123,13 +3135,15 @@ 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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (isrec, elim, indsign) = Tacmach.New.of_old (get_eliminator elim) gl in
let names = compute_induction_names (Array.length indsign) names in
(if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
(Tacticals.New.tclTHEN
(induct_tac elim)
(Proofview.V82.tactic (tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps))))
(Array.map2 (induct_discharge destopt avoid tac) indsign names)
+ end
(* Apply induction "in place" taking into account dependent
hypotheses from the context *)
@@ -3218,8 +3232,11 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
+ let reduce_to_quantified_ref =
+ Tacmach.New.pf_apply reduce_to_quantified_ref gl
+ in
try (* reduce_to_quantified_ref can raise an exception *)
let typ0 = reduce_to_quantified_ref indref tmptyp0 in
let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
@@ -3231,19 +3248,23 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
apply_induction_in_context
(Some (hyp0,inhyps)) elim indvars names induct_tac
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let elim_info = Tacmach.New.of_old (find_induction_type isrec elim hyp0) gl in
Tacticals.New.tclTHEN
(atomize_param_of_ind elim_info hyp0)
(induction_from_context isrec with_evars elim_info
(hyp0,lbind) names inhyps)
+ end
(* Induction on a list of induction arguments. Analyse the elim
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) ->
+ Proofview.Goal.enter begin fun gl ->
+ let (indsign,scheme as elim_info) = Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) gl in
let awaited_nargs =
scheme.nparams + scheme.nargs
+ (if scheme.farg_in_concl then 1 else 0)
@@ -3253,6 +3274,7 @@ let induction_without_atomization isrec with_evars elim names lid =
if not (Int.equal nlid awaited_nargs)
then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments."))
else induction_from_context_l with_evars elim_info lid names
+ end
let has_selected_occurrences = function
| None -> false
@@ -3301,7 +3323,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
let env = Proofview.Goal.env gl in
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 ->
+ let id = Tacmach.New.of_old (fresh_id [] x) gl in
(* 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 *)
@@ -3339,19 +3361,21 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
try (* type_of can raise an exception *)
let x =
id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
- Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
+ let id = Tacmach.New.of_old (fresh_id [] x) gl in
let newl' = List.map (replace_term c (mkVar id)) l' in
let _ = newlc:=id::!newlc in
let _ = letids:=id::!letids in
Tacticals.New.tclTHEN
(letin_tac None (Name id) c None allHypsAndConcl)
(atomize_list newl')
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end in
Tacticals.New.tclTHENLIST
[
(atomize_list lc);
@@ -3370,7 +3394,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let ifi = Tacmach.New.of_old (is_functional_induction elim) gl in
if Int.equal (List.length lc) 1 && not ifi then
(* standard induction *)
onOpenInductionArg
@@ -3385,7 +3410,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 ->
+ let finish_evar_resolution = Tacmach.New.pf_apply finish_evar_resolution gl in
let lc = List.map
(map_induction_arg finish_evar_resolution) lc in
begin match lc with
@@ -3407,6 +3432,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
new_induct_gen_l isrec with_evars elim names newlc
end
end
+ end
let induction_destruct isrec with_evars = function
| [],_,_ -> Proofview.tclUNIT ()
@@ -3494,13 +3520,15 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let t = Tacmach.New.pf_get_hyp_typ id gl in
+ let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
if is_conjunction (hnf_constr t) then
(Tacticals.New.tclTHEN (simplest_elim (mkVar id)) (Tacticals.New.tclDO 2 intro))
else
Proofview.tclZERO (Errors.UserError (
"andE" , (str("Tactic andE expects "^(Id.to_string id)^" is a conjunction."))))
+ end
let dAnd cls =
Tacticals.New.onClause
@@ -3510,13 +3538,15 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let t = Tacmach.New.pf_get_hyp_typ id gl in
+ let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
if is_disjunction (hnf_constr t) then
(Tacticals.New.tclTHEN (simplest_elim (mkVar id)) intro)
else
Proofview.tclZERO (Errors.UserError (
"orE" , (str("Tactic orE expects "^(Id.to_string id)^" is a disjunction."))))
+ end
let dorE b cls =
Tacticals.New.onClause
@@ -3526,8 +3556,9 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let t = Tacmach.New.pf_get_hyp_typ id gl in
+ let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
if is_imp_term (hnf_constr t) then
let (dom, _, rng) = destProd (hnf_constr t) in
Tacticals.New.tclTHENLAST
@@ -3537,6 +3568,7 @@ let impE id =
Proofview.tclZERO (Errors.UserError (
"impE" , (str("Tactic impE expects "^(Id.to_string id)^
" is a an implication."))))
+ end
let dImp cls =
Tacticals.New.onClause
@@ -3644,7 +3676,8 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
let symmetry_in id =
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
try (* type_of can raise an exception *)
let ctype = type_of (mkVar id) in
let sign,t = decompose_prod_assum ctype in
@@ -3664,6 +3697,7 @@ let symmetry_in id =
| e -> Proofview.tclZERO e
end
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let intros_symmetry =
Tacticals.New.onClause
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index bc756eb82..c3d83b394 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -351,7 +351,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
)))
)
in
- Tacmach.New.of_old (fun gl -> pf_type_of gl p) >>= fun type_of_pq ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
try
@@ -380,6 +381,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (Tactics.emit_side_effects eff);
Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
+ end
(* used in the bool -> leib side *)
let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
@@ -410,7 +412,8 @@ 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 ->
+ Proofview.Goal.enter begin fun gl ->
+ let type_of = Tacmach.New.pf_apply Typing.type_of gl in
begin try (* type_of can raise an exception *)
let tt1 = type_of t1 in
if eq_constr t1 t2 then aux q1 q2
@@ -454,6 +457,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
)
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
+ end
| ([],[]) -> Proofview.tclUNIT ()
| _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 04:02:45 +0000