aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/omega/coq_omega.ml8
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrtacticals.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/tactics.ml16
-rw-r--r--tactics/tactics.mli2
8 files changed, 20 insertions, 20 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 523c7c8305..ec5e46d89b 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -184,7 +184,7 @@ END
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast }
END
{
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d40ba6562..99a9c1ab9a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
| Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+ convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
beta_hyp id
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
@@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
end
| None, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_concl_no_check newt DEFAULTcast
+ convert_concl ~check:false newt DEFAULTcast
in
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4802608fda..f3bc791b8d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -535,7 +535,7 @@ let focused_simpl path =
let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
- convert_concl_no_check newc DEFAULTcast
+ convert_concl ~check:false newc DEFAULTcast
end
let focused_simpl path = focused_simpl path
@@ -687,7 +687,7 @@ let simpl_coeffs path_init path_k =
let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
in
- convert_concl_no_check newc DEFAULTcast
+ convert_concl ~check:false newc DEFAULTcast
end
let rec shuffle p (t1,t2) =
@@ -1849,12 +1849,12 @@ let destructure_hyps =
match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
- (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
decl))
(loop lit))
| Kapp(Z,_) ->
(tclTHEN
- (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
decl))
(loop lit))
| _ -> loop lit
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 2a84469af0..f9b3284037 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -426,7 +426,7 @@ let mk_anon_id t gl_ids =
(set s i (Char.chr (Char.code (get s i) + 1)); s) in
Id.of_string_soft (Bytes.to_string (loop (n - 1)))
-let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast
+let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast
let convert_concl t = Tactics.convert_concl t DEFAULTcast
let rename_hd_prod orig_name_ref gl =
@@ -1408,8 +1408,6 @@ let tclINTRO_ANON ?seed () =
| Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return
let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
- let convert_concl_no_check t =
- Tactics.convert_concl_no_check t DEFAULTcast in
let concl = Goal.concl gl in
let sigma = Goal.sigma gl in
match EConstr.kind sigma concl with
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index bbe7bde78b..17e4114958 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
| _ -> EConstr.map (project gl) unmark c in
let utac hyp =
Proofview.V82.of_tactic
- (Tactics.convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in
+ (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in
let utacs = List.map utac (pf_hyps gl) in
let ugtac gl' =
Proofview.V82.of_tactic
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3019fc0231..70854e6e3c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -515,6 +515,6 @@ let autounfold_one db cl =
if did then
match cl with
| Some hyp -> change_in_hyp None (make_change_arg c') hyp
- | None -> convert_concl_no_check c' DEFAULTcast
+ | None -> convert_concl ~check:false c' DEFAULTcast
else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 066b9c7794..60027b06e8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -697,7 +697,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
let reduct_in_concl (redfun,sty) =
Proofview.Goal.enter begin fun gl ->
- convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
+ convert_concl ~check:false (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
end
let reduct_in_hyp ?(check=false) redfun (id,where) =
@@ -756,7 +756,7 @@ let e_change_in_concl (redfun,sty) =
let sigma = Proofview.Goal.sigma gl in
let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (convert_concl_no_check c sty)
+ (convert_concl ~check:false c sty)
end
let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
@@ -2174,7 +2174,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
check_number_of_constructors expctdnumopt i nconstr;
Tacticals.New.tclTHENLIST [
- convert_concl_no_check redcl DEFAULTcast;
+ convert_concl ~check:false redcl DEFAULTcast;
intros;
constructor_core with_evars (ind, i) lbind
]
@@ -2203,7 +2203,7 @@ let any_constructor with_evars tacopt =
Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
if Int.equal nconstr 0 then error "The type has no constructors.";
Tacticals.New.tclTHENLIST [
- convert_concl_no_check redcl DEFAULTcast;
+ convert_concl ~check:false redcl DEFAULTcast;
intros;
any_constr ind nconstr 1 ()
]
@@ -2647,9 +2647,9 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
in
Tacticals.New.tclTHENLIST
[ Proofview.Unsafe.tclEVARS sigma;
- convert_concl_no_check newcl DEFAULTcast;
+ convert_concl ~check:false newcl DEFAULTcast;
intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
- Tacticals.New.tclMAP convert_hyp_no_check depdecls;
+ Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls;
eq_tac ]
end
@@ -4799,7 +4799,7 @@ let symmetry_red allowred =
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
- (convert_concl_no_check concl DEFAULTcast)
+ (convert_concl ~check:false concl DEFAULTcast)
(Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
end
@@ -4894,7 +4894,7 @@ let transitivity_red allowred t =
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
- (convert_concl_no_check concl DEFAULTcast)
+ (convert_concl ~check:false concl DEFAULTcast)
(match t with
| None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
| Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 75b5caaa36..e545ec9b5f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -36,7 +36,9 @@ val introduction : Id.t -> unit Proofview.tactic
val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_concl]"]
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
val fix : Id.t -> int -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:59:22 +0000