aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--plugins/firstorder/formula.ml6
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml9
-rw-r--r--plugins/funind/glob_term_to_relation.ml10
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/indfun_common.mli9
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/g_class.mlg13
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/rtauto/Bintree.v8
-rw-r--r--plugins/setoid_ring/Field_theory.v4
-rw-r--r--plugins/setoid_ring/Ring_polynom.v4
-rw-r--r--plugins/ssr/ssrbool.v38
-rw-r--r--plugins/ssr/ssrelim.ml3
-rw-r--r--plugins/ssr/ssrvernac.mlg4
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
19 files changed, 77 insertions, 57 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 204f889f90..ef6c07bff2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1044,7 +1044,9 @@ let fake_match_projection env p =
let indu = mkIndU (ind,u) in
let ctx, paramslet =
let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
- let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in
+ let (ctx, cty) = mip.mind_nf_lc.(0) in
+ let cty = Term.it_mkProd_or_LetIn cty ctx in
+ let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in
List.chop mip.mind_consnrealdecls.(0) rctx
in
let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index a60a966cec..56b3dc97cf 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -13,7 +13,6 @@ open Names
open Constr
open EConstr
open Vars
-open Termops
open Util
open Declarations
open Globnames
@@ -100,9 +99,8 @@ let kind_of_formula env sigma term =
else
let has_realargs=(n>0) in
let is_trivial=
- let is_constant c =
- Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
- Array.exists is_constant mip.mind_nf_lc in
+ let is_constant n = Int.equal n 0 in
+ Array.exists is_constant mip.mind_consnrealargs in
if Inductiveops.mis_is_recursive (ind,mib,mip) ||
(has_realargs && not is_trivial)
then
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
raise NoChange;
end
in
- let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+ let eq_constr c1 c2 =
+ try ignore(Evarconv.unify_delay env sigma c1 c2); true
+ with Evarconv.UnableToUnify _ -> false in
if not (noccurn sigma 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp sigma t) then nochange "not an equality";
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 25a7675113..ca09cad1f3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
in
let names = ref [new_princ_name] in
let hook =
- fun new_principle_type _ _ ->
+ fun new_principle_type _ _ _ _ ->
if Option.is_empty sorts
then
(* let id_of_f = Label.to_id (con_label f) in *)
@@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
- save false new_princ_name entry g_kind ~hook
+ let uctx = Evd.evar_universe_context sigma in
+ save false new_princ_name entry ~hook uctx g_kind
with e when CErrors.noncritical e ->
begin
begin
@@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
this_block_funs
0
(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
- (fun _ _ _ -> ())
+ (fun _ _ _ _ _ -> ())
with e when CErrors.noncritical e ->
begin
begin
@@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
this_block_funs
!i
(prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
- (fun _ _ _ -> ())
+ (fun _ _ _ _ _ -> ())
in
const
with Found_type i ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 02964d7ba5..ba0a3bbb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl =
construct
in
let argl =
- if List.is_empty argl
- then
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
- )
- else argl
+ if List.is_empty argl then
+ List.make cst_narg (mkGHole ())
+ else
+ List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f9938c0356..cba3cc3d42 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
| Local -> true
| Global -> false
-let save with_clean id const ?hook (locality,_,kind) =
+let save with_clean id const ?hook uctx (locality,_,kind) =
let fix_exn = Future.fix_exn_of const.const_entry_body in
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
@@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) =
(locality, ConstRef kn)
in
if with_clean then Proof_global.discard_current ();
- Lemmas.call_hook ?hook ~fix_exn l r;
+ Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
definition_message id
let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 9584649cff..1e0b95df34 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,7 +42,14 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *)
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
-val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit
+val save
+ : bool
+ -> Id.t
+ -> Safe_typing.private_constants Entries.definition_entry
+ -> ?hook:Lemmas.declaration_hook
+ -> UState.t
+ -> Decl_kinds.goal_kind
+ -> unit
(* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a8517e9ab1..8746c37309 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let na = next_global_ident_away name Id.Set.empty in
if Termops.occur_existential sigma gls_type then
CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
- let hook _ _ =
+ let hook _ _ _ _ =
let opacity =
let na_ref = qualid_of_ident na in
let na_global = Smartlocate.global_with_alias na_ref in
@@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
- let hook _ _ =
+ let hook _ _ _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 9ecc36bdf3..3f2fabeeee 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -99,8 +99,19 @@ TACTIC EXTEND is_ground
| [ "is_ground" constr(ty) ] -> { is_ground ty }
END
+{
+let deprecated_autoapply_using =
+ CWarnings.create
+ ~name:"autoapply-using" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.")
+}
+
TACTIC EXTEND autoapply
-| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i }
+| [ "autoapply" constr(c) "using" preident(i) ] -> {
+ deprecated_autoapply_using ();
+ autoapply c i
+ }
+| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i }
END
{
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7da4464e59..e78d0f93a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
unsolvable constraints remain, so we check that this unification
does not introduce any new problem. *)
let _, pbs = Evd.extract_all_conv_pbs evd in
- let evd' = Evarconv.the_conv_x env x y evd in
+ let evd' = Evarconv.unify_delay env evd x y in
let _, pbs' = Evd.extract_all_conv_pbs evd' in
if evd' == evd || problem_inclusion pbs' pbs then Some evd'
else None
@@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n =
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
- let hook _ = function
+ let hook _ _ _ = function
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 30f716d764..eac84f0543 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
let c_interp patvars env sigma =
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 751f0d8334..c2dec264ad 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -294,10 +294,10 @@ Qed.
End Store.
-Arguments PNone [A].
+Arguments PNone {A}.
Arguments PSome [A] _.
-Arguments Tempty [A].
+Arguments Tempty {A}.
Arguments Branch0 [A] _ _.
Arguments Branch1 [A] _ _ _.
@@ -311,7 +311,7 @@ Arguments mkStore [A] index contents.
Arguments index [A] s.
Arguments contents [A] s.
-Arguments empty [A].
+Arguments empty {A}.
Arguments get [A] i S.
Arguments push [A] a S.
@@ -319,7 +319,7 @@ Arguments get_empty [A] i.
Arguments get_push_Full [A] i a S _.
Arguments Full [A] _.
-Arguments F_empty [A].
+Arguments F_empty {A}.
Arguments F_push [A] a S _.
Arguments In [A] x S F.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index dba72337b2..f5d13053b1 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1789,5 +1789,5 @@ End Field.
End Complete.
-Arguments FEO [C].
-Arguments FEI [C].
+Arguments FEO {C}.
+Arguments FEI {C}.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9ef24144d2..12f716c496 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1507,5 +1507,5 @@ Qed.
End MakeRingPol.
-Arguments PEO [C].
-Arguments PEI [C].
+Arguments PEO {C}.
+Arguments PEI {C}.
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index ed4ff2aa66..d6b7371647 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -813,21 +813,21 @@ Proof. by case b1; case b2; constructor; auto. Qed.
End ReflectConnectives.
-Arguments idP [b1].
-Arguments idPn [b1].
-Arguments negP [b1].
-Arguments negPn [b1].
-Arguments negPf [b1].
-Arguments andP [b1 b2].
-Arguments and3P [b1 b2 b3].
-Arguments and4P [b1 b2 b3 b4].
-Arguments and5P [b1 b2 b3 b4 b5].
-Arguments orP [b1 b2].
-Arguments or3P [b1 b2 b3].
-Arguments or4P [b1 b2 b3 b4].
-Arguments nandP [b1 b2].
-Arguments norP [b1 b2].
-Arguments implyP [b1 b2].
+Arguments idP {b1}.
+Arguments idPn {b1}.
+Arguments negP {b1}.
+Arguments negPn {b1}.
+Arguments negPf {b1}.
+Arguments andP {b1 b2}.
+Arguments and3P {b1 b2 b3}.
+Arguments and4P {b1 b2 b3 b4}.
+Arguments and5P {b1 b2 b3 b4 b5}.
+Arguments orP {b1 b2}.
+Arguments or3P {b1 b2 b3}.
+Arguments or4P {b1 b2 b3 b4}.
+Arguments nandP {b1 b2}.
+Arguments norP {b1 b2}.
+Arguments implyP {b1 b2}.
Prenex Implicits idP idPn negP negPn negPf.
Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
@@ -953,7 +953,7 @@ Proof. by case: a; case: b. Qed.
Lemma addbP a b : reflect (~~ a = b) (a (+) b).
Proof. by case: a; case: b; constructor. Qed.
-Arguments addbP [a b].
+Arguments addbP {a b}.
(**
Resolution tactic for blindly weeding out common terms from boolean
@@ -1158,8 +1158,8 @@ Definition clone_pred U :=
End Predicates.
-Arguments pred0 [T].
-Arguments predT [T].
+Arguments pred0 {T}.
+Arguments predT {T}.
Prenex Implicits pred0 predT predI predU predC predD preim relU.
Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B))
@@ -1357,7 +1357,7 @@ Variant qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x => let: Qualifier _ p := q in p x.
-Arguments has_quality n [T].
+Arguments has_quality n {T}.
Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a0b1d784f1..7216849948 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let mind,indb = Inductive.lookup_mind_specif env (kn,i) in
let tys = indb.Declarations.mind_nf_lc in
let renamed_tys =
- Array.mapi (fun j t ->
+ Array.mapi (fun j (ctx, cty) ->
+ let t = Term.it_mkProd_or_LetIn cty ctx in
ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
let t = Arguments_renaming.rename_type t
(GlobRef.ConstructRef((kn,i),j+1)) in
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d083d34b52..2e1554d496 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -152,7 +152,7 @@ let declare_one_prenex_implicit locality f =
with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
let rec loop = function
| a :: args' when Impargs.is_status_implicit a ->
- (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
+ Impargs.MaximallyImplicit :: loop args'
| args' when List.exists Impargs.is_status_implicit args' ->
errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
| _ -> [] in
@@ -165,7 +165,7 @@ let declare_one_prenex_implicit locality f =
| [] ->
errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| impls ->
- Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
+ Impargs.set_implicits locality fref [impls]
}
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 552a4048b1..fb99b87108 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a =
loop 0
let unif_HO env ise p c =
- try Evarconv.the_conv_x env p c ise
+ try Evarconv.unify_delay env ise p c
with Evarconv.UnableToUnify(ise, err) ->
raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:08:32 +0000