aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/Algebra.v24
-rw-r--r--plugins/ltac/extraargs.ml420
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/romega/ReflOmegaCore.v2
-rw-r--r--plugins/romega/g_romega.mlg8
-rw-r--r--plugins/setoid_ring/Field_theory.v3
-rw-r--r--plugins/setoid_ring/Ncring_initial.v5
-rw-r--r--plugins/ssr/ssreflect.v3
-rw-r--r--plugins/ssr/ssrelim.ml6
-rw-r--r--plugins/ssr/ssrequality.ml3
-rw-r--r--plugins/ssr/ssrfun.v2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml5
-rw-r--r--plugins/ssrmatching/ssrmatching.v4
13 files changed, 64 insertions, 23 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index ee7341a4a2..f1095fc9f1 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Omega ROmega.
+Require Import Bool PArith DecidableClass Omega Lia.
Ltac bool :=
repeat match goal with
@@ -84,9 +84,9 @@ Ltac case_decide := match goal with
let H := fresh "H" in
define (@decide P D) b H; destruct b; try_decide
| [ |- context [Pos.compare ?x ?y] ] =>
- destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
+ destruct (Pos.compare_spec x y); try lia
| [ X : context [Pos.compare ?x ?y] |- _ ] =>
- destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
+ destruct (Pos.compare_spec x y); try lia
end.
Section Definitions.
@@ -325,13 +325,13 @@ Qed.
Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p.
Proof.
-intros k l p H; revert l; induction H; constructor; eauto; zify; romega.
+intros k l p H; revert l; induction H; constructor; eauto; lia.
Qed.
Lemma linear_valid_incl : forall k p, linear k p -> valid k p.
Proof.
intros k p H; induction H; constructor; auto.
-eapply valid_le_compat; eauto; zify; romega.
+eapply valid_le_compat; eauto; lia.
Qed.
End Validity.
@@ -417,13 +417,13 @@ Qed.
Hint Extern 5 =>
match goal with
| [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
- apply Pos.max_case_strong; intros; zify; romega
+ apply Pos.max_case_strong; intros; lia
| [ |- (?z <= Pos.max ?x ?y)%positive ] =>
- apply Pos.max_case_strong; intros; zify; romega
+ apply Pos.max_case_strong; intros; lia
| [ |- (Pos.max ?x ?y < ?z)%positive ] =>
- apply Pos.max_case_strong; intros; zify; romega
+ apply Pos.max_case_strong; intros; lia
| [ |- (?z < Pos.max ?x ?y)%positive ] =>
- apply Pos.max_case_strong; intros; zify; romega
+ apply Pos.max_case_strong; intros; lia
| _ => zify; omega
end.
Hint Resolve Pos.le_max_r Pos.le_max_l.
@@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl.
now rewrite <- (Pos.max_id i); intuition.
destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
+ apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto.
- + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega.
- + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega.
+ + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia.
+ + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia.
+ apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition.
+ apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition.
}
@@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c
Proof.
intros k v p H; induction H; simpl; [now auto|].
case_decide; [|now auto].
-eapply (valid_le_compat i); [now auto|zify; romega].
+eapply (valid_le_compat i); [now auto|lia].
Qed.
Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index d779951180..38600695dc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -199,9 +199,9 @@ let pr_gen_place pr_id = function
ConclLocation () -> Pp.mt ()
| HypLocation (id,InHyp) -> str "in " ++ pr_id id
| HypLocation (id,InHypTypeOnly) ->
- str "in (Type of " ++ pr_id id ++ str ")"
+ str "in (type of " ++ pr_id id ++ str ")"
| HypLocation (id,InHypValueOnly) ->
- str "in (Value of " ++ pr_id id ++ str ")"
+ str "in (value of " ++ pr_id id ++ str ")"
let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id)
let pr_place _ _ _ = pr_gen_place Id.print
@@ -220,6 +220,14 @@ let interp_place ist gl p =
let subst_place subst pl = pl
+let warn_deprecated_instantiate_syntax =
+ CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated"
+ (fun (v,v',id) ->
+ let s = Id.to_string id in
+ Pp.strbrk
+ ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".")
+ )
+
ARGUMENT EXTEND hloc
PRINTED BY pr_place
INTERPRETED BY interp_place
@@ -234,8 +242,14 @@ ARGUMENT EXTEND hloc
| [ "in" ident(id) ] ->
[ HypLocation ((CAst.make id),InHyp) ]
| [ "in" "(" "Type" "of" ident(id) ")" ] ->
- [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+ [ warn_deprecated_instantiate_syntax ("Type","type",id);
+ HypLocation ((CAst.make id),InHypTypeOnly) ]
| [ "in" "(" "Value" "of" ident(id) ")" ] ->
+ [ warn_deprecated_instantiate_syntax ("Value","value",id);
+ HypLocation ((CAst.make id),InHypValueOnly) ]
+| [ "in" "(" "type" "of" ident(id) ")" ] ->
+ [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+| [ "in" "(" "value" "of" ident(id) ")" ] ->
[ HypLocation ((CAst.make id),InHypValueOnly) ]
END
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..f4313a8fa3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,7 @@ let _ =
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
in
- Pretyping.register_constr_interp0 wit_tactic eval
+ GlobEnv.register_constr_interp0 wit_tactic eval
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b9935..da86f4274d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -8,6 +8,7 @@
*************************************************************************)
Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
+Declare Scope Int_scope.
Delimit Scope Int_scope with I.
(** * Abstract Integers. *)
@@ -716,6 +717,7 @@ Inductive term : Set :=
| Topp : term -> term
| Tvar : N -> term.
+Declare Scope romega_scope.
Bind Scope romega_scope with term.
Delimit Scope romega_scope with term.
Arguments Tint _%I.
diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
index c1ce30027e..ac4f30b1db 100644
--- a/plugins/romega/g_romega.mlg
+++ b/plugins/romega/g_romega.mlg
@@ -41,14 +41,22 @@ let romega_tactic unsafe l =
(Tactics.intros)
(total_reflexive_omega_tactic unsafe))
+let romega_depr =
+ Vernacinterp.mk_deprecation
+ ~since:(Some "8.9")
+ ~note:(Some "Use lia instead.")
+ ()
+
}
TACTIC EXTEND romega
+DEPRECATED { romega_depr }
| [ "romega" ] -> { romega_tactic false [] }
| [ "unsafe_romega" ] -> { romega_tactic true [] }
END
TACTIC EXTEND romega'
+DEPRECATED { romega_depr }
| [ "romega" "with" ne_ident_list(l) ] ->
{ romega_tactic false (List.map Names.Id.to_string l) }
| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d9e32dbbf8..ce115f564f 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -19,6 +19,7 @@ Section MakeFieldPol.
(* Field elements : R *)
Variable R:Type.
+Declare Scope R_scope.
Bind Scope R_scope with R.
Delimit Scope R_scope with ring.
Local Open Scope R_scope.
@@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth.
(* Coefficients : C *)
Variable C: Type.
+Declare Scope C_scope.
Bind Scope C_scope with C.
Delimit Scope C_scope with coef.
@@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N).
(* Polynomial expressions : (PExpr C) *)
+Declare Scope PE_scope.
Bind Scope PE_scope with PExpr.
Delimit Scope PE_scope with poly.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 523c7b02eb..1ca6227f25 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}.
| Z0 => 0
| Zneg p => -(gen_phiPOS p)
end.
- Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
- Local Open Scope ZMORPHISM.
+ Declare Scope ZMORPHISM.
+ Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Open Scope ZMORPHISM.
Definition get_signZ z :=
match z with
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b4144aa45e..460bdc6d23 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -86,6 +86,7 @@ Export SsrSyntax.
(* recognize the expansion of the boolean if; using the default printer *)
(* avoids a spurrious trailing %GEN_IF. *)
+Declare Scope general_if_scope.
Delimit Scope general_if_scope with GEN_IF.
Notation "'if' c 'then' v1 'else' v2" :=
@@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
(* Force boolean interpretation of simple if expressions. *)
+Declare Scope boolean_if_scope.
Delimit Scope boolean_if_scope with BOOL_IF.
Notation "'if' c 'return' t 'then' v1 'else' v2" :=
@@ -125,6 +127,7 @@ Open Scope boolean_if_scope.
(* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *)
(* Lists library) should be loaded before ssreflect so that their notations *)
(* do not mask all ssreflect forms. *)
+Declare Scope form_scope.
Delimit Scope form_scope with FORM.
Open Scope form_scope.
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index fbe3b000fb..602fcfcab5 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -293,7 +293,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let c, cl, ucst = match_pat env p occ h cl in
let gl = pf_merge_uc ucst gl in
let c = EConstr.of_constr c in
- let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in
+ let gl = try pf_unify_HO gl inf_t c
+ with exn when CErrors.noncritical exn -> error gl c inf_t in
cl, gl, post
with
| NoMatch | NoProgress ->
@@ -302,7 +303,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let e = EConstr.of_constr e in
let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in
let e, _, _, gl = pf_saturate ~beta:true gl e n in
- let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in
+ let gl = try pf_unify_HO gl inf_t e
+ with exn when CErrors.noncritical exn -> error gl e inf_t in
cl, gl, post
in
let rec match_all concl gl patterns =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 23cbf49c05..f23433f2f4 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -115,7 +115,8 @@ let newssrcongrtac arg ist gl =
(* utils *)
let fs gl t = Reductionops.nf_evar (project gl) t in
let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
- match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with
+ 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)))
(t_ok (proj gl_c)) gl
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index b2d5143e36..99ff943e61 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -216,6 +216,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+Declare Scope fun_scope.
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
@@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y)
Notation "@^~ x" := (fun f => f x)
(at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope.
+Declare Scope pair_scope.
Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 30a998c6ce..20ea8b3667 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -291,7 +291,10 @@ let unif_EQ_args env sigma pa a =
prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a
;;
-let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
+let unif_HO env ise p c =
+ try Evarconv.the_conv_x env p c ise
+ with Evarconv.UnableToUnify(ise, err) ->
+ raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))
let unif_HO_args env ise0 pa i ca =
let n = Array.length pa in
diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v
index 829ee05e11..9a53e1dd1a 100644
--- a/plugins/ssrmatching/ssrmatching.v
+++ b/plugins/ssrmatching/ssrmatching.v
@@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0).
Reserved Notation "( a 'in' b 'in' c )" (at level 0).
Reserved Notation "( a 'as' b 'in' c )" (at level 0).
+Declare Scope ssrpatternscope.
+Delimit Scope ssrpatternscope with pattern.
+
(* Notation to define shortcuts for the "X in t" part of a pattern. *)
Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
-Delimit Scope ssrpatternscope with pattern.
(* Some shortcuts for recurrent "X in t" parts. *)
Notation RHS := (X in _ = X)%pattern.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 22:35:29 +0000