aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/recdef.ml32
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--plugins/setoid_ring/Field_theory.v41
-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.ml14
-rw-r--r--plugins/ssr/ssrfwd.ml6
-rw-r--r--plugins/ssr/ssrtacticals.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
12 files changed, 78 insertions, 49 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3c2b03dfe0..1fca132655 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -132,7 +132,7 @@ let nat = function () -> (coq_init_constant "nat")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
let eq = function () -> (coq_init_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -145,7 +145,7 @@ let coq_O = function () -> (coq_init_constant "O")
let coq_S = function () -> (coq_init_constant "S")
let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
let max_ref = function () -> (find_reference ["Recdef"] "max")
-let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
+let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
let f_S t = mkApp(delayed_force coq_S, [|t|]);;
@@ -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
@@ -1041,13 +1041,13 @@ let compute_terminate_type nb_args func =
let open Term in
let open Constr in
let open CVars in
- let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
+ let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_monomorphic_global func)) in
let rev_args,b = decompose_prod_n nb_args a_arrow_b in
let left =
mkApp(delayed_force iter_rd,
Array.of_list
(lift 5 a_arrow_b:: mkRel 3::
- constr_of_global func::mkRel 1::
+ constr_of_monomorphic_global func::mkRel 1::
List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
)
)
@@ -1065,7 +1065,7 @@ let compute_terminate_type nb_args func =
delayed_force nat,
(mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
mkArrow cond Sorts.Relevant result))))|])in
- let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
+ let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref),
[|b;
(mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
compose_prod rev_args value
@@ -1161,7 +1161,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
fun g ->
let sigma = project g in
let ids = Termops.ids_of_named_context (pf_hyps g) in
- let func_body = (def_of_const (constr_of_global func)) in
+ let func_body = (def_of_const (constr_of_monomorphic_global func)) in
let func_body = EConstr.of_constr func_body in
let (f_name, _, body1) = destLambda sigma func_body in
let f_id =
@@ -1222,7 +1222,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types pstate =
let p = Proof_global.give_me_the_proof pstate in
- let sgs,_,_,_,sigma = Proof.proof p in
+ let Proof.{ goals=sgs; sigma; _ } = Proof.data p in
sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
@@ -1253,7 +1253,7 @@ let build_and_l sigma l =
let c,tac,nb = f pl in
mk_and p1 c,
tclTHENS
- (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr))))
+ (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr))))
[tclIDTAC;
tac
],nb+1
@@ -1437,7 +1437,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
(cont_tactic:Id.t list -> tactic) g =
let sigma = project g in
let ids = pf_ids_of_hyps g in
- let terminate_constr = constr_of_global term_f in
+ let terminate_constr = constr_of_monomorphic_global term_f in
let terminate_constr = EConstr.of_constr terminate_constr in
let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in
let x = n_x_id ids nargs in
@@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
let evd = Evd.from_ctx uctx in
- let f_constr = constr_of_global f_ref in
+ let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
@@ -1466,12 +1466,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
(fun x ->
prove_eq (fun _ -> tclIDTAC)
{nb_arg=nb_arg;
- f_terminate = EConstr.of_constr (constr_of_global terminate_ref);
+ f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref);
f_constr = EConstr.of_constr f_constr;
concl_tac = tclIDTAC;
func=functional_ref;
info=(instantiate_lambda Evd.empty
- (EConstr.of_constr (def_of_const (constr_of_global functional_ref)))
+ (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref)))
(EConstr.of_constr f_constr::List.map mkVar x)
);
is_main_branch = true;
@@ -1570,9 +1570,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
if not stop
then
let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
- let f_ref = destConst (constr_of_global f_ref)
- and functional_ref = destConst (constr_of_global functional_ref)
- and eq_ref = destConst (constr_of_global eq_ref) in
+ let f_ref = destConst (constr_of_monomorphic_global f_ref)
+ and functional_ref = destConst (constr_of_monomorphic_global functional_ref)
+ and eq_ref = destConst (constr_of_monomorphic_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
functional_ref eq_ref rec_arg_num
(EConstr.of_constr rec_arg_type)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 99a9c1ab9a..a68efa4713 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 ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
@@ -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 ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+ convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
beta_hyp id
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ef6af16036..de9dec0f74 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -207,7 +207,7 @@ struct
* ZMicromega.v
*)
- let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+ let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n)
let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
[@@@ocaml.warning "+3"]
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f3bc791b8d..ffc3506a1f 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1849,12 +1849,12 @@ let destructure_hyps =
match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
- (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
decl))
(loop lit))
| Kapp(Z,_) ->
(tclTHEN
- (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
decl))
(loop lit))
| _ -> loop lit
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 813c521ab0..ad2ee821b3 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1235,12 +1235,19 @@ Notation ring_correct :=
(ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
(* simplify a field expression into a fraction *)
-(* TODO: simplify when den is constant... *)
Definition display_linear l num den :=
- NPphi_dev l num / NPphi_dev l den.
+ let lnum := NPphi_dev l num in
+ match den with
+ | Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den
+ | _ => lnum / NPphi_dev l den
+ end.
Definition display_pow_linear l num den :=
- NPphi_pow l num / NPphi_pow l den.
+ let lnum := NPphi_pow l num in
+ match den with
+ | Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den
+ | _ => lnum / NPphi_pow l den
+ end.
Theorem Field_rw_correct n lpe l :
Ninterp_PElist l lpe ->
@@ -1252,7 +1259,18 @@ Theorem Field_rw_correct n lpe l :
Proof.
intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
rewrite (Fnorm_FEeval_PEeval _ _ H).
- unfold display_linear; apply rdiv_ext;
+ unfold display_linear.
+ destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
+ try ( apply rdiv_ext;
+ eapply ring_rw_correct; eauto).
+ destruct (ceqb_spec c cI).
+ set (nnum := NPphi_dev _ _).
+ apply eq_trans with (nnum / NPphi_dev l (Pc c)).
+ apply rdiv_ext;
+ eapply ring_rw_correct; eauto.
+ rewrite Pphi_dev_ok; try eassumption.
+ now simpl; rewrite H0, phi_1, <- rdiv1.
+ apply rdiv_ext;
eapply ring_rw_correct; eauto.
Qed.
@@ -1266,8 +1284,19 @@ Theorem Field_rw_pow_correct n lpe l :
Proof.
intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
rewrite (Fnorm_FEeval_PEeval _ _ H).
- unfold display_pow_linear; apply rdiv_ext;
- eapply ring_rw_pow_correct;eauto.
+ unfold display_pow_linear.
+ destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
+ try ( apply rdiv_ext;
+ eapply ring_rw_pow_correct; eauto).
+ destruct (ceqb_spec c cI).
+ set (nnum := NPphi_pow _ _).
+ apply eq_trans with (nnum / NPphi_pow l (Pc c)).
+ apply rdiv_ext;
+ eapply ring_rw_pow_correct; eauto.
+ rewrite Pphi_pow_ok; try eassumption.
+ now simpl; rewrite H0, phi_1, <- rdiv1.
+ apply rdiv_ext;
+ eapply ring_rw_pow_correct; eauto.
Qed.
Theorem Field_correct n l lpe fe1 fe2 :
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..93c0d5c236 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 =
@@ -446,7 +446,7 @@ let lz_setoid_relation =
| Some (env', srel) when env' == env -> srel
| _ ->
let srel =
- try Some (UnivGen.constr_of_global @@
+ try Some (UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
with _ -> None in
last_srel := Some (env, srel); srel
@@ -491,7 +491,7 @@ let rwprocess_rule dir rule gl =
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
EConstr.mkApp (pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then
+ if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
@@ -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/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 17e4114958..91ff432364 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 ~check:false (NamedDecl.map_constr unmark hyp)) in
+ (Tactics.convert_hyp ~check:false ~reorder: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/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 () =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 23:27:46 +0000