Drop support for Rocq 9.0

.nix/config.nix

@@ -354,41 +354,5 @@ with builtins; with (import <nixpkgs> {}).lib;
       VST.job = false;  # depends on compcert
     } // listToAttrs (forEach lighten-released (p:
       { name = p; value.job = false; })); };
-    "rocq-9.0" = { rocqPackages = common-bundles // {
-      rocq-core.override.version = "9.0.0";
-      # check that we compile without warnings on last release of Coq
-      stdlib-warnings.job = true;
-      # plugin pins, from v9.0 branch of Coq
-      bignums.override.version = "cc2d9ee990e4cfebe5f107d8357198baa526eded";
-      stdlib-test.job = false;
-    }; coqPackages = coq-common-bundles // {
-      coq.override.version = "9.0.0";
-      # plugin pins, from v9.0 branch of Coq
-      aac-tactics.override.version = "109af844f39bf541823271e45e42e40069f3c2c4";
-      atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543";
-      bignums.override.version = "cc2d9ee990e4cfebe5f107d8357198baa526eded";
-      bignums-test.override.version = "cc2d9ee990e4cfebe5f107d8357198baa526eded";
-      itauto.job = false;  # broken
-      coinduction.override.version = "09caaf1f809e3e91ebba05bc38cef6de83ede3b3";
-      dpdgraph-test.override.version = "74ced1b11a8df8d4c04c3829fcf273aa63d2c493";
-      coq-hammer.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
-      coq-hammer-tactics.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
-      equations.override.version = "1.3.1+9.0";
-      equations-test.job = false;
-      fiat-parsers.job = false;  # broken
-      metarocq.override.version = "1.4-9.0";
-      mtac2.override.version = "1cdb2cb628444ffe9abc6535f6d2e11004de7fc1";
-      paramcoq-test.override.version = "32609ca4a9bf4a0e456a855ea5118d8c00cda6be";
-      relation-algebra.override.version = "7966d1a7bb524444120c56c3474717bcc91a5215";
-      rocq-lean-import.override.version = "c513cee4f5edf8e8a06ba553ca58de5142cffde6";
-      smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
-      # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
-      stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
-      unicoq.override.version = "a9b72f755539c0b3280e38e778a09e2b7519a51a";
-      waterproof.override.version = "443f794ddc102309d00f1d512ab50b84fdc261aa";
-      compcert.job = false;  # broken
-      VST.job = false;  # depends on compcert
-    } // listToAttrs (forEach lighten-released (p:
-      { name = p; value.job = false; })); };
   };
 }

rocq-stdlib.opam

@@ -25,7 +25,7 @@ bug-reports: "https://github.com/coq/stdlib/issues"
 dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
   "rocq-runtime"
-  "rocq-core" {>= "9.0"}
+  "rocq-core" {>= "9.1"}
 ]
 build: [
   [make "-j" jobs]

rocq-stdlib.opam.template

@@ -1,6 +1,6 @@
 depends: [
   "rocq-runtime"
-  "rocq-core" {>= "9.0"}
+  "rocq-core" {>= "9.1"}
 ]
 build: [
   [make "-j" jobs]

theories/Reals/Nsatz.v

@@ -1,4 +1,4 @@
-Attributes deprecated(since="9.1", note="Use RNsatz, QNsatz, or ZNsatz, or NsatzTactic.").
+Attributes deprecated(since="Stdlib 9.1", note="Use RNsatz, QNsatz, or ZNsatz, or NsatzTactic.").
 Require Export RNsatz QNsatz ZNsatz NsatzTactic.
 
 From Stdlib Require Import List.
@@ -37,16 +37,16 @@ Ltac Ncring_tac.extra_reify term ::=
   | _ => open_constr:(tt)
   end.
 
-#[deprecated(since="9.1", note="use discriminate")]
+#[deprecated(since="Stdlib 9.1", note="use discriminate")]
 Lemma Z_one_zero: 1%Z <> 0%Z.
 Proof. discriminate. Qed.
 
-#[deprecated(since="9.1", use=Q_apart_0_1)]
+#[deprecated(since="Stdlib 9.1", use=Q_apart_0_1)]
 Notation Q_one_zero := Q_apart_0_1 (only parsing).
 
-#[deprecated(since="9.1", use=eq_equivalence)]
+#[deprecated(since="Stdlib 9.1", use=eq_equivalence)]
 Lemma Rsth : Setoid_Theory R (@eq R).
 Proof. cbv [Setoid_Theory]. exact _. Qed.
 
-#[deprecated(since="9.1", use=R1_neq_R0)]
+#[deprecated(since="Stdlib 9.1", use=R1_neq_R0)]
 Notation R_one_zero := R1_neq_R0 (only parsing).

theories/Reals/RIneq.v

@@ -2685,7 +2685,7 @@ Proof.
 Qed.
 
 (* NOTE: keeping inconsistent variable names for backward compatibility. *)
-#[deprecated(use=Z.eqb_eq, since="9.0")]
+#[deprecated(use=Z.eqb_eq, since="Stdlib 9.0")]
 Lemma Zeq_bool_IZR : forall x y:Z, IZR x = IZR y -> Z.eqb x y = true.
 Proof. now intros n m H; apply Z.eqb_eq, eq_IZR. Qed.
 

theories/Sorting/Permutation.v

@@ -884,6 +884,6 @@ Qed.
 End Permutation_transp.
 
 (* begin hide *)
-#[deprecated(since="9.1", use=Permutation_app_comm )]
+#[deprecated(since="Stdlib 9.1", use=Permutation_app_comm )]
 Notation Permutation_app_swap := Permutation_app_comm (only parsing).
 (* end hide *)

theories/ZArith/BinInt.v

@@ -1871,11 +1871,11 @@ Qed.
 
 End LocalNotations.
 
-#[deprecated(since="9.0")]
+#[deprecated(since="Stdlib 9.0")]
 Notation SYM1 lem := (fun n => eq_sym (lem n)) (only parsing).
-#[deprecated(since="9.0")]
+#[deprecated(since="Stdlib 9.0")]
 Notation SYM2 lem := (fun n m => eq_sym (lem n m)) (only parsing).
-#[deprecated(since="9.0")]
+#[deprecated(since="Stdlib 9.0")]
 Notation SYM3 lem := (fun n m p => eq_sym (lem n m p)) (only parsing).
 
 #[global]

theories/ZArith/ZArith.v

@@ -56,5 +56,5 @@ From Stdlib Require Export ZNsatz.
 
 Export ZArithRing.
 
-(* This compat Require is deprecated since 9.1 *)
+(* This compat Require is deprecated since Stdlib 9.1 *)
 From Stdlib Require Znumtheory.

theories/ZArith/ZArith_base.v

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Attributes deprecated(since="9.0", note="use ZArith instead").
+Attributes deprecated(since="Stdlib 9.0", note="use ZArith instead").
 
 (** Library for manipulating integers based on binary encoding.
     This is a subset of basic modules.

theories/ZArith/Zbool.v

@@ -131,64 +131,64 @@ Qed.
 (** The decidability of equality and order relations over
     type [Z] gives some boolean functions with the adequate specification. *)
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y).
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y).
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y).
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y).
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z.eq_dec x y).
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y).
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
 
 (**********************************************************************)
 (** * Boolean comparisons of binary integers *)
 
-#[deprecated(use=Z.leb, since="9.0")]
+#[deprecated(use=Z.leb, since="Stdlib 9.0")]
 Notation Zle_bool := Z.leb (only parsing).
-#[deprecated(use=Z.geb, since="9.0")]
+#[deprecated(use=Z.geb, since="Stdlib 9.0")]
 Notation Zge_bool := Z.geb (only parsing).
-#[deprecated(use=Z.ltb, since="9.0")]
+#[deprecated(use=Z.ltb, since="Stdlib 9.0")]
 Notation Zlt_bool := Z.ltb (only parsing).
-#[deprecated(use=Z.gtb, since="9.0")]
+#[deprecated(use=Z.gtb, since="Stdlib 9.0")]
 Notation Zgt_bool := Z.gtb (only parsing).
 
 (** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare].
    The old [Zeq_bool] is kept for compatibility. *)
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Notation Zeq_bool := Z.eqb.
 
-#[deprecated(use=Z.eqb_eq, since="9.0")]
+#[deprecated(use=Z.eqb_eq, since="Stdlib 9.0")]
 Lemma Zeq_is_eq_bool x y : x = y <-> Zeq_bool x y = true.
 Proof. symmetry; apply Z.eqb_eq. Qed.
 
-#[deprecated(use=Z.eqb_eq, since="9.0")]
+#[deprecated(use=Z.eqb_eq, since="Stdlib 9.0")]
 Lemma Zeq_bool_eq x y : Zeq_bool x y = true -> x = y.
 Proof. apply Z.eqb_eq. Qed.
 
-#[deprecated(use=Z.eqb, since="9.0")]
+#[deprecated(use=Z.eqb, since="Stdlib 9.0")]
 Definition Zneq_bool (x y:Z) :=
   match x ?= y with
     | Eq => false
     | _ => true
   end.
 
-#[deprecated(use=Z.eqb_eq, since="9.0")]
+#[deprecated(use=Z.eqb_eq, since="Stdlib 9.0")]
 Lemma Zeq_bool_neq x y : Zeq_bool x y = false -> x <> y.
 Proof.
  rewrite Zeq_is_eq_bool; now destruct Zeq_bool.
 Qed.
 
-#[deprecated(use=Z.eqb_eq, since="9.0")]
+#[deprecated(use=Z.eqb_eq, since="Stdlib 9.0")]
 Lemma Zeq_bool_if x y : if Zeq_bool x y then x=y else x<>y.
 Proof.
  generalize (Zeq_bool_eq x y) (Zeq_bool_neq x y).

theories/ZArith/Zcomplements.v

@@ -20,7 +20,7 @@ From Stdlib Require Zeven.
 (**********************************************************************)
 (** About parity *)
 
-#[deprecated(since="9.0")]
+#[deprecated(since="Stdlib 9.0")]
 Notation two_or_two_plus_one := Zeven.Z_modulo_2 (only parsing).
 
 (**********************************************************************)

theories/ZArith/Zdiv.v

@@ -192,7 +192,7 @@ Proof.
   intros a; destruct a; simpl; auto.
 Qed.
 
-#[deprecated(use=Z.mod_0_r, since="9.1")]
+#[deprecated(use=Z.mod_0_r, since="Stdlib 9.1")]
 Lemma Zmod_0_r: forall a, a mod 0 = a.
 Proof.
   intros a; destruct a; simpl; auto.
@@ -203,7 +203,7 @@ Proof.
   intros a; destruct a; simpl; auto.
 Qed.
 
-#[deprecated(use=Z.div_0_r, since="9.1")]
+#[deprecated(use=Z.div_0_r, since="Stdlib 9.1")]
 Lemma Zdiv_0_r: forall a, a/0 = 0.
 Proof.
   intros a; destruct a; simpl; auto.