aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--plugins/ssr/ssrcommon.ml12
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrequality.ml10
-rw-r--r--plugins/ssr/ssrfwd.ml6
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/tactics.ml72
-rw-r--r--tactics/tactics.mli18
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
13 files changed, 70 insertions, 70 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3c2b03dfe0..3dd3a430e8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -701,7 +701,7 @@ let mkDestructEq :
let changefun patvars env sigma =
pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
in
- Proofview.V82.of_tactic (change_in_concl None changefun) g2);
+ Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 99a9c1ab9a..355c16bfd0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1574,8 +1574,8 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
(* For compatibility *)
- let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
- let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
+ let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
+ let beta_hyp id = Tactics.reduct_in_hyp ~check:false Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 3f69701bd3..b02b97f656 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -89,10 +89,10 @@ let protect_red map env sigma c0 =
EConstr.of_constr (eval 0 c)
let protect_tac map =
- Tactics.reduct_option (protect_red map,DEFAULTcast) None
+ Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
+ Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
(****************************************************************************)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a4caeb403c..56f17703ff 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -427,7 +427,7 @@ let mk_anon_id t gl_ids =
Id.of_string_soft (Bytes.to_string (loop (n - 1)))
let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast
-let convert_concl t = Tactics.convert_concl t DEFAULTcast
+let convert_concl ~check t = Tactics.convert_concl ~check t DEFAULTcast
let rename_hd_prod orig_name_ref gl =
match EConstr.kind (project gl) (pf_concl gl) with
@@ -799,7 +799,7 @@ let discharge_hyp (id', (id, mode)) gl =
| NamedDecl.LocalDef (_, v, t), _ ->
let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in
Proofview.V82.of_tactic
- (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl
+ (convert_concl ~check:true (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl
(* wildcard names *)
let clear_wilds wilds gl =
@@ -1170,7 +1170,7 @@ let gentac gen gl =
ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
let gl = pf_merge_uc ucst gl in
if conv
- then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (old_cleartac clr) gl
+ then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
else genclrtac cl [c] clr gl
let genstac (gens, clr) =
@@ -1215,7 +1215,7 @@ let unprotecttac gl =
let prot, _ = EConstr.destConst (project gl) c in
Tacticals.onClause (fun idopt ->
let hyploc = Option.map (fun id -> id, InHyp) idopt in
- Proofview.V82.of_tactic (Tactics.reduct_option
+ Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
(Reductionops.clos_norm_flags
(CClosure.RedFlags.mkflags
[CClosure.RedFlags.fBETA;
@@ -1282,10 +1282,10 @@ let clr_of_wgen gen clrs = match gen with
| clr, _ -> old_cleartac clr :: clrs
-let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast)
+let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast)
let unfold cl =
let module R = Reductionops in let module F = CClosure.RedFlags in
- reduct_in_concl (R.clos_norm_flags (F.mkflags
+ reduct_in_concl ~check:false (R.clos_norm_flags (F.mkflags
(List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @
[F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX])))
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 58ce84ecb3..575f016014 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -252,7 +252,7 @@ val ssrevaltac :
Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic
val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
-val convert_concl : EConstr.t -> unit Proofview.tactic
+val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic
val red_safe :
Reductionops.reduction_function ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ad20113320..e349031952 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -118,7 +118,7 @@ let newssrcongrtac arg ist gl =
match try Some (pf_unify_HO gl_c (pf_concl gl) c)
with exn when CErrors.noncritical exn -> None with
| Some gl_c ->
- tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c)))
+ tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c)))
(t_ok (proj gl_c)) gl
| None -> t_fail () gl in
let mk_evar gl ty =
@@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl =
try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold))
with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in
let _ = conclude () in
- Proofview.V82.of_tactic (convert_concl concl) gl
+ Proofview.V82.of_tactic (convert_concl ~check:true concl) gl
;;
let foldtac occ rdx ft gl =
@@ -303,7 +303,7 @@ let foldtac occ rdx ft gl =
let concl0 = EConstr.Unsafe.to_constr concl0 in
let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
let _ = conclude () in
- Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl
+ Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl
;;
let converse_dir = function L2R -> R2L | R2L -> L2R
@@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr 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 cl'), rewritetac ?under dir r', gl
+ Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl
else
let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
let r3, _, r3t =
@@ -644,7 +644,7 @@ let unfoldtac occ ko t kt gl =
let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in
let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
Proofview.V82.of_tactic
- (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
+ (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
let unlocktac ist args gl =
let utac (occ, gt) gl =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 01d71aa96a..4d4400a0f8 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -56,7 +56,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
| 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 cl')) (introid id) gl
+ Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl
open Util
@@ -161,7 +161,7 @@ let havetac ist
let gl, ty = pfe_type_of gl t in
let ctx, _ = EConstr.decompose_prod_n_assum (project gl) 1 ty in
let assert_is_conv gl =
- try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
+ try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl
with _ -> errorstrm (str "Given proof term is not of type " ++
pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in
gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
@@ -471,7 +471,7 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
if hint = nohint then
Proofview.tclUNIT ()
else
- let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+ let betaiota = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
(* Usefulness of check_numgoals: tclDISPATCH would be enough,
except for the error message w.r.t. the number of
provided/expected tactics, as the last one is implied *)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 1deb935d5c..4e0866a0c5 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1299,7 +1299,7 @@ let ssrpatterntac _ist arg gl =
let concl_x = EConstr.of_constr concl_x in
let gl, tty = pf_type_of gl t in
let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in
- Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
+ Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl
(* Register "ssrpattern" tactic *)
let () =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 70854e6e3c..0857c05968 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -514,7 +514,7 @@ let autounfold_one db cl =
in
if did then
match cl with
- | Some hyp -> change_in_hyp None (make_change_arg c') hyp
+ | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
| None -> convert_concl ~check:false c' DEFAULTcast
else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3d760f1c3d..f049f8c568 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1613,10 +1613,10 @@ let cutSubstInHyp l2r eqn id =
tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(tclTHENFIRST
(tclTHENLIST [
- (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
+ (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly));
(replace_core (onHyp id) l2r eqn)
])
- (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+ (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly)))
end
let try_rewrite tac =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5a19f95f90..78e7ce2321 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -145,7 +145,7 @@ let introduction id =
let error msg = CErrors.user_err Pp.(str msg)
-let convert_concl ?(check=true) ty k =
+let convert_concl ~check ty k =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let conclty = Proofview.Goal.concl gl in
@@ -163,7 +163,7 @@ let convert_concl ?(check=true) ty k =
end
end
-let convert_hyp ?(check=true) d =
+let convert_hyp ~check d =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -701,7 +701,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
(** Tactic reduction modulo evars (for universes essentially) *)
-let e_change_in_concl ?(check = false) (redfun, sty) =
+let e_change_in_concl ~check (redfun, sty) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -709,7 +709,7 @@ let e_change_in_concl ?(check = false) (redfun, sty) =
(convert_concl ~check c' sty)
end
-let e_change_in_hyp ?(check = false) redfun (id,where) =
+let e_change_in_hyp ~check redfun (id,where) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let hyp = Tacmach.New.pf_get_hyp id gl in
@@ -718,7 +718,7 @@ let e_change_in_hyp ?(check = false) redfun (id,where) =
(convert_hyp ~check c)
end
-let e_change_in_hyps ?(check=true) f args =
+let e_change_in_hyps ~check f args =
Proofview.Goal.enter begin fun gl ->
let fold (env, sigma) arg =
let (redfun, id, where) = f arg in
@@ -745,26 +745,26 @@ let e_change_in_hyps ?(check=true) f args =
let e_reduct_in_concl = e_change_in_concl
-let reduct_in_concl ?(check = false) (redfun, sty) =
+let reduct_in_concl ~check (redfun, sty) =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_change_in_concl ~check (redfun, sty)
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_reduct_in_hyp ~check redfun (id, where) =
let redfun _ env sigma c = redfun env sigma c in
e_change_in_hyp ~check redfun (id, where)
-let reduct_in_hyp ?(check = false) redfun (id, where) =
+let reduct_in_hyp ~check redfun (id, where) =
let redfun _ env sigma c = (sigma, redfun env sigma c) in
e_change_in_hyp ~check redfun (id, where)
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
-let e_reduct_option ?(check=false) redfun = function
+let e_reduct_option ~check redfun = function
| Some id -> e_reduct_in_hyp ~check (fst redfun) id
| None -> e_change_in_concl ~check (revert_cast redfun)
-let reduct_option ?(check = false) (redfun, sty) where =
+let reduct_option ~check (redfun, sty) where =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_reduct_option ~check (redfun, sty) where
@@ -802,7 +802,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
| Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm check cv_pb deep t where env sigma c =
+let change_on_subterm ~check cv_pb deep t where env sigma c =
let mayneedglobalcheck = ref false in
let (sigma, c) = match where with
| None ->
@@ -825,15 +825,15 @@ let change_on_subterm check cv_pb deep t where env sigma c =
end;
(sigma, c)
-let change_in_concl ?(check=true) occl t =
+let change_in_concl ~check occl t =
(* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
- e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
+ e_change_in_concl ~check:false ((change_on_subterm ~check Reduction.CUMUL false t occl),DEFAULTcast)
-let change_in_hyp ?(check=true) occl t id =
+let change_in_hyp ~check occl t id =
(* FIXME: we set the [check] flag only to reorder hypotheses in case of
introduction of dependencies in new variables. We should separate this
check from the conversion function. *)
- e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id
+ e_change_in_hyp ~check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -842,7 +842,7 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with
| Some l ->
List.map (fun ((occs, id), w) -> (id, occs, w)) l
-let change ?(check=true) chg c cls =
+let change ~check chg c cls =
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
begin match cls.concl_occs with
@@ -852,7 +852,7 @@ let change ?(check=true) chg c cls =
<*>
let f (id, occs, where) =
let occl = bind_change_occurrences occs chg in
- let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
+ let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
e_change_in_hyps ~check f hyps
@@ -862,23 +862,23 @@ let change_concl t =
change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let red_in_concl = reduct_in_concl (red_product,REVERTcast)
-let red_in_hyp = reduct_in_hyp red_product
-let red_option = reduct_option (red_product,REVERTcast)
-let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast)
-let hnf_in_hyp = reduct_in_hyp hnf_constr
-let hnf_option = reduct_option (hnf_constr,REVERTcast)
-let simpl_in_concl = reduct_in_concl (simpl,REVERTcast)
-let simpl_in_hyp = reduct_in_hyp simpl
-let simpl_option = reduct_option (simpl,REVERTcast)
-let normalise_in_concl = reduct_in_concl (compute,REVERTcast)
-let normalise_in_hyp = reduct_in_hyp compute
-let normalise_option = reduct_option (compute,REVERTcast)
-let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
-let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
-let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
-let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
+let red_in_concl = reduct_in_concl ~check:false (red_product,REVERTcast)
+let red_in_hyp = reduct_in_hyp ~check:false red_product
+let red_option = reduct_option ~check:false (red_product,REVERTcast)
+let hnf_in_concl = reduct_in_concl ~check:false (hnf_constr,REVERTcast)
+let hnf_in_hyp = reduct_in_hyp ~check:false hnf_constr
+let hnf_option = reduct_option ~check:false (hnf_constr,REVERTcast)
+let simpl_in_concl = reduct_in_concl ~check:false (simpl,REVERTcast)
+let simpl_in_hyp = reduct_in_hyp ~check:false simpl
+let simpl_option = reduct_option ~check:false (simpl,REVERTcast)
+let normalise_in_concl = reduct_in_concl ~check:false (compute,REVERTcast)
+let normalise_in_hyp = reduct_in_hyp ~check:false compute
+let normalise_option = reduct_option ~check:false (compute,REVERTcast)
+let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast)
+let unfold_in_hyp loccname = reduct_in_hyp ~check:false (unfoldn loccname)
+let unfold_option loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast)
+let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast)
(* The main reduction function *)
@@ -3061,8 +3061,8 @@ let unfold_body x =
Tacticals.New.afterHyp x begin fun aft ->
let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
let rfun _ _ c = replace_vars [x, xval] c in
- let reducth h = reduct_in_hyp rfun h in
- let reductc = reduct_in_concl (rfun, DEFAULTcast) in
+ let reducth h = reduct_in_hyp ~check:false rfun h in
+ let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in
Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
end
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b3914816ac..3bb9a34509 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -33,8 +33,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
(** {6 Primitive tactics. } *)
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 : 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
@@ -152,13 +152,13 @@ type e_tactic_reduction = Reductionops.e_reduction_function
type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
val make_change_arg : constr -> change_arg
-val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
-val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val reduct_in_hyp : check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_option : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
+val reduct_in_concl : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
+val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val change_in_concl : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : constr -> unit Proofview.tactic
-val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp : check:bool -> (occurrences * constr_pattern) option -> change_arg ->
hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : hyp_location -> unit Proofview.tactic
@@ -180,7 +180,7 @@ val unfold_in_hyp :
val unfold_option :
(occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
val change :
- ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+ check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 603e00c815..a8c1a67f6f 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -167,7 +167,7 @@ let change pat c cl =
delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma
in
let cl = mk_clause cl in
- Tactics.change pat c cl
+ Tactics.change ~check:true pat c cl
end
let rewrite ev rw cl by =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:29:23 +0000