aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ssr/ssrbwd.ml12
-rw-r--r--plugins/ssr/ssrcommon.ml23
-rw-r--r--plugins/ssr/ssrcommon.mli4
-rw-r--r--plugins/ssr/ssrelim.ml4
-rw-r--r--plugins/ssr/ssrequality.ml12
-rw-r--r--plugins/ssr/ssrfwd.ml68
-rw-r--r--plugins/ssr/ssrfwd.mli2
-rw-r--r--plugins/ssr/ssrtacticals.ml4
8 files changed, 72 insertions, 57 deletions
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 0674d3d28a..32a215444b 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -119,11 +119,13 @@ let refine_interp_apply_view dbl ist gl gv =
else [])
let apply_top_tac =
- Tacticals.tclTHENLIST [
+ Proofview.Goal.enter begin fun _ ->
+ Tacticals.New.tclTHENLIST [
introid top_id;
- apply_rconstr (mkRVar top_id);
- old_cleartac [SsrHyp(None,top_id)]
+ Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
+ cleartac [SsrHyp(None,top_id)]
]
+ end
let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
let _, clr = interp_hyps ist gl gclr in
@@ -150,7 +152,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
let gl = pf_merge_uc_of sigma gl in
Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl
| _, _ ->
- Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
+ Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl
)
-let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
+let apply_top_tac = apply_top_tac
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 6ab0a16789..29f52d8834 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1060,23 +1060,24 @@ let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
else Tacticals.New.tclTHEN Tactics.hnf_in_concl (fst_prod true tac)
end
-let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl ->
- let g, env = Tacmach.pf_concl gl, pf_env gl in
- let sigma = project gl in
+let introid ?(orig=ref Anonymous) name =
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let g = Proofview.Goal.concl gl in
match EConstr.kind sigma g with
| App (hd, _) when EConstr.isLambda sigma hd ->
- Proofview.V82.of_tactic (convert_concl_no_check (Reductionops.whd_beta sigma g)) gl
- | _ -> tclIDTAC gl)
- (Proofview.V82.of_tactic
- (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name)))
-;;
+ convert_concl_no_check (Reductionops.whd_beta sigma g)
+ | _ -> Tacticals.New.tclIDTAC
+ end <*>
+ (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))
let anontac decl gl =
let id = match RelDecl.get_name decl with
| Name id ->
if is_discharged_id id then id else mk_anon_id (Id.to_string id) (Tacmach.pf_ids_of_hyps gl)
| _ -> mk_anon_id ssr_anon_hyp (Tacmach.pf_ids_of_hyps gl) in
- introid id gl
+ Proofview.V82.of_tactic (introid id) gl
let rec intro_anon gl =
try anontac (List.hd (fst (EConstr.decompose_prod_n_assum (project gl) 1 (Tacmach.pf_concl gl)))) gl
@@ -1314,8 +1315,8 @@ let abs_wgen keep_let f gen (gl,args,c) =
let clr_of_wgen gen clrs = match gen with
| clr, Some ((x, _), None) ->
let x = hoi_id x in
- old_cleartac clr :: old_cleartac [SsrHyp(Loc.tag x)] :: clrs
- | clr, _ -> old_cleartac clr :: clrs
+ cleartac clr :: cleartac [SsrHyp(Loc.tag x)] :: clrs
+ | clr, _ -> cleartac clr :: clrs
let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 5db55eca91..362e488d8a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -398,7 +398,7 @@ val pfLIFT
(** Basic tactics *)
-val introid : ?orig:Name.t ref -> Id.t -> v82tac
+val introid : ?orig:Name.t ref -> Id.t -> unit Proofview.tactic
val intro_anon : v82tac
val interp_clr :
@@ -427,7 +427,7 @@ val abs_wgen :
val clr_of_wgen :
ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option ->
- Proofview.V82.tac list -> Proofview.V82.tac list
+ unit Proofview.tactic list -> unit Proofview.tactic list
val unfold : EConstr.t list -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b3fa1ea9d0..6155f8fbf6 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -519,8 +519,8 @@ let perform_injection c =
let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in
let id = injecteq_id in
let id_with_ebind = (EConstr.mkVar id, NoBindings) in
- let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
- Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
+ let injtac = Tacticals.New.tclTHEN (introid id) (Proofview.V82.tactic (injectidl2rtac id id_with_ebind)) in
+ Proofview.V82.of_tactic (Tacticals.New.tclTHENLAST (Tactics.apply (EConstr.compose_lam dc cl1)) injtac) gl
end
let ssrscase_or_inj_tac c =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index c2ee180855..1e3e2e69ea 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -420,12 +420,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
| AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
let new_rdx = if dir = L2R then a.(2) else a.(1) in
- pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
+ pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, Tacticals.New.tclIDTAC, gl
| _ ->
let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
let sigma, _ = Typing.type_of env sigma cl' in
let gl = pf_merge_uc_of sigma gl in
- Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl
+ Proofview.V82.of_tactic (convert_concl ~check:true cl'), Proofview.V82.tactic (rewritetac ?under dir r'), gl
else
let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
let r3, _, r3t =
@@ -435,9 +435,9 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
let itacs = [introid pattern_id; introid rule_id] in
- let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
- let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
- apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
+ let cltac = Tactics.clear [pattern_id; rule_id] in
+ let rwtacs = [Proofview.V82.tactic (rewritetac ?under dir (EConstr.mkVar rule_id)); cltac] in
+ apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), gl
in
let cvtac' _ =
try cvtac gl with
@@ -452,7 +452,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
(EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl)
++ error)
in
- tclTHEN cvtac' rwtac gl
+ tclTHEN cvtac' (Proofview.V82.of_tactic rwtac) gl
[@@@ocaml.warning "-3"]
let lz_coq_prod =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 708833c52f..8173db000a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -59,7 +59,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) =
| Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
| _ -> c, pfe_type_of gl c in
let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in
- Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl
+ Proofview.V82.of_tactic (Tacticals.New.tclTHEN (convert_concl ~check:true cl') (introid id)) gl
end
open Util
@@ -89,11 +89,17 @@ let combineCG t1 t2 f g = match t1, t2 with
| _, (_, (_, None)) -> anomaly "have: mixed C-G constr"
| _ -> anomaly "have: mixed G-C constr"
-let basecuttac name c gl =
- let hd, gl = pf_mkSsrConst name gl in
+let basecuttac name c =
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, hd = mkSsrConst name env sigma in
let t = EConstr.mkApp (hd, [|c|]) in
- let gl, _ = pf_e_type_of gl t in
- Proofview.V82.of_tactic (Tactics.apply t) gl
+ let sigma, _ = Typing.type_of env sigma t in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Tactics.apply t
+ end
let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
@@ -123,13 +129,19 @@ let havetac ist
not !ssrhaveNOtcresolution &&
match fk with FwdHint(_,true) -> false | _ -> true in
let hint = Proofview.V82.of_tactic (hinttac ist true hint) in
- let cuttac t gl =
+ let cuttac t =
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
if transp then
- let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, have_let = mkSsrConst "ssr_have_let" env sigma in
let step = EConstr.mkApp (have_let, [|concl;t|]) in
- let gl, _ = pf_e_type_of gl step in
- Proofview.V82.of_tactic (applyn ~with_evars:true ~with_shelve:false 2 step) gl
- else basecuttac "ssr_have" t gl in
+ let sigma, _ = Typing.type_of env sigma step in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ applyn ~with_evars:true ~with_shelve:false 2 step
+ else basecuttac "ssr_have" t
+ end in
(* Introduce now abstract constants, so that everything sees them *)
let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
let unlock_abs (idty,args_id) gl =
@@ -203,7 +215,7 @@ let havetac ist
let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac
| _, true, false -> assert false in
- Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
+ Tacticals.tclTHENS (Proofview.V82.of_tactic (cuttac cut)) [ Tacticals.tclTHEN sol itac1; itac2 ] gl)
gl
end
@@ -264,41 +276,41 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
| LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
| _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
c, args, pired c args, pf_merge_uc uc gl in
- let tacipat pats = introstac pats in
+ let tacipat pats = Proofview.V82.tactic (introstac pats) in
let tacigens =
- Tacticals.tclTHEN
- (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
- (introstac (List.fold_right mkpats gens [])) in
- let hinttac = Proofview.V82.of_tactic (hinttac ist true hint) in
+ Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0])))
+ (Proofview.V82.tactic (introstac (List.fold_right mkpats gens []))) in
+ let hinttac = hinttac ist true hint in
let cut_kind, fst_goal_tac, snd_goal_tac =
match suff, ghave with
- | true, `NoGen -> "ssr_wlog", Tacticals.tclTHEN hinttac (tacipat pats), tacigens
- | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.tclTHEN tacigens (tacipat pats)
+ | true, `NoGen -> "ssr_wlog", Tacticals.New.tclTHEN hinttac (tacipat pats), tacigens
+ | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.New.tclTHEN tacigens (tacipat pats)
| true, `Gen _ -> assert false
| false, `Gen id ->
if gens = [] then errorstrm(str"gen have requires some generalizations");
- let clear0 = old_cleartac clr0 in
+ let clear0 = cleartac clr0 in
let id, name_general_hyp, cleanup, pats = match id, pats with
| None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats
- | None, _ -> None, Tacticals.tclIDTAC, clear0, pats
+ | None, _ -> None, Tacticals.New.tclIDTAC, clear0, pats
| Some (Some id),_ -> Some id, introid id, clear0, pats
| Some _,_ ->
let id = mk_anon_id "tmp" (Tacmach.pf_ids_of_hyps gl) in
- Some id, introid id, Tacticals.tclTHEN clear0 (Proofview.V82.of_tactic (Tactics.clear [id])), pats in
+ Some id, introid id, Tacticals.New.tclTHEN clear0 (Tactics.clear [id]), pats in
let tac_specialize = match id with
- | None -> Tacticals.tclIDTAC
+ | None -> Tacticals.New.tclIDTAC
| Some id ->
- if pats = [] then Tacticals.tclIDTAC else
+ if pats = [] then Tacticals.New.tclIDTAC else
let args = Array.of_list args in
ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
- Tacticals.tclTHENS (basecuttac "ssr_have" ct)
- [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in
+ Tacticals.New.tclTHENS (basecuttac "ssr_have" ct)
+ [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in
"ssr_have",
(if hint = nohint then tacigens else hinttac),
- Tacticals.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup]
+ Tacticals.New.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup]
in
- Tacticals.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl
+ Proofview.V82.of_tactic (Tacticals.New.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac]) gl
end
(** The "suffice" tactic *)
@@ -324,7 +336,7 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
in
let ctac gl =
let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
- basecuttac "ssr_suff" ty gl in
+ Proofview.V82.of_tactic (basecuttac "ssr_suff" ty) gl in
Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
end
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 2de10837c5..dc90b159d7 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -31,7 +31,7 @@ val havetac : ist ->
val basecuttac :
string ->
- EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
+ EConstr.t -> unit Proofview.tactic
val wlogtac :
Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 4f9747ae73..a379b2561a 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -132,7 +132,7 @@ let tclCLAUSES tac (gens, clseq) =
Proofview.V82.tactic begin fun gl ->
if clseq = InGoal || clseq = InSeqGoal then tac gl else
let clr_gens = pf_clauseids gl gens clseq in
- let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
+ let clear = Tacticals.New.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in
let cl0 = pf_concl gl in
let dtac gl =
@@ -145,7 +145,7 @@ let tclCLAUSES tac (gens, clseq) =
| _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id)
| _, None -> None) gens in
endclausestac id_map clseq gl_id cl0 in
- Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl
+ Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; Proofview.V82.of_tactic clear; tac; endtac]) gl
end
(** The "do" tactical. ********************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:42:15 +0000