Deprecate duplicated definitions

.github/workflows/docker-action.yml

@@ -45,17 +45,19 @@ jobs:
             endGroup
 
             startGroup "Test dependants"
+              opam install conf-clang
               PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
               PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
               for PACKAGE in $PACKAGES
               do DEPS_FAILED=false
-                 opam install -y --deps-only $PACKAGE || DEPS_FAILED=true
+                 opam install --deps-only $PACKAGE || DEPS_FAILED=true
                  [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
               done
             endGroup
-          export: 'OPAMWITHTEST'
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
         env:
           OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
       - name: Revert permissions
         # to avoid a warning at cleanup time
         if: ${{ always() }}

theories/Data/Char.v

@@ -6,7 +6,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition ascii_dec (l r : Ascii.ascii) : bool :=
+Definition deprecated_ascii_dec (l r : Ascii.ascii) : bool :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
@@ -28,7 +28,10 @@ Definition ascii_dec (l r : Ascii.ascii) : bool :=
         else false
   end.
 
-Theorem ascii_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use Ascii.eqb instead.")]
+Notation ascii_dec := deprecated_ascii_dec.
+
+Theorem deprecated_ascii_dec_sound : forall l r,
   ascii_dec l r = true <-> l = r.
 Proof.
   unfold ascii_dec. intros.
@@ -39,17 +42,20 @@ Proof.
          end; split; congruence.
 Qed.
 
+#[deprecated(since="8.9",note="Use Ascii.eqb_eq instead.")]
+Notation ascii_dec_sound := deprecated_ascii_dec_sound.
+
 Global Instance RelDec_ascii : RelDec (@eq Ascii.ascii) :=
-{ rel_dec := ascii_dec }.
+{ rel_dec := Ascii.eqb }.
 
 Global Instance RelDec_Correct_ascii : RelDec_Correct RelDec_ascii.
 Proof.
-  constructor; auto using ascii_dec_sound.
+  constructor; auto using Ascii.eqb_eq.
 Qed.
 
-Global Instance Reflect_ascii_dec a b : Reflect (ascii_dec a b) (a = b) (a <> b).
+Global Instance Reflect_ascii_dec a b : Reflect (Ascii.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using ascii_dec_sound.
+  apply iff_to_reflect; auto using Ascii.eqb_eq.
 Qed.
 
 Definition digit2ascii (n:nat) : Ascii.ascii :=

theories/Data/String.v

@@ -18,72 +18,77 @@ Local Notation "x >> y" := (match x with
                               | z => z
                             end) (only parsing, at level 30).
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.12",note="Use Bool.compare instead.")] *)
-Definition bool_cmp (l r : bool) : comparison :=
+Definition deprecated_bool_cmp (l r : bool) : comparison :=
   match l , r with
     | true , false => Gt
     | false , true => Lt
     | true , true
     | false , false => Eq
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use Ascii.compare instead.")] *)
-Definition ascii_cmp (l r : Ascii.ascii) : comparison :=
+#[deprecated(since="8.12",note="Use Bool.compare instead.")]
+Notation bool_cmp := deprecated_bool_cmp.
+
+Definition deprecated_ascii_cmp (l r : Ascii.ascii) : comparison :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
       bool_cmp l8 r8 >> bool_cmp l7 r7 >> bool_cmp l6 r6 >> bool_cmp l5 r5 >>
       bool_cmp l4 r4 >> bool_cmp l3 r3 >> bool_cmp l2 r2 >> bool_cmp l1 r1
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb instead.")] *)
-Fixpoint string_dec (l r : string) : bool :=
+#[deprecated(since="8.15",note="Use Ascii.compare instead.")]
+Notation ascii_cmp := deprecated_ascii_cmp.
+
+Fixpoint deprecated_string_dec (l r : string) : bool :=
   match l , r with
     | EmptyString , EmptyString => true
     | String l ls , String r rs =>
-      if ascii_dec l r then string_dec ls rs
+      if Ascii.eqb l r then deprecated_string_dec ls rs
       else false
     | _ , _ => false
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb_spec instead.")] *)
-Theorem string_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use String.eqb instead.")]
+Notation string_dec := deprecated_string_dec.
+
+Theorem deprecated_string_dec_sound : forall l r,
   string_dec l r = true <-> l = r.
 Proof.
-  induction l; destruct r; simpl; split; try solve [ intuition ; congruence ];
-  consider (ascii_dec a a0); intros; subst. f_equal. eapply IHl; auto.
-  apply IHl. congruence.
-  inversion H. congruence.
+  induction l; destruct r; try (constructor; easy); simpl.
+  case (Ascii.eqb_spec a a0); simpl; [intros -> | constructor; now intros [= ]].
+  case (IHl r); intros; constructor; intros; f_equal; auto.
+  inversion H1; subst; auto.
 Qed.
 
+#[deprecated(since="8.9",note="Use String.eqb_eq instead.")]
+Notation string_dec_sound := deprecated_string_dec_sound.
+
 Global Instance RelDec_string : RelDec (@eq string) :=
-{| rel_dec := string_dec |}.
+{| rel_dec := String.eqb |}.
 
 Global Instance RelDec_Correct_string : RelDec_Correct RelDec_string.
 Proof.
-  constructor; auto using string_dec_sound.
+  constructor; auto using String.eqb_eq.
 Qed.
 
-Global Instance Reflect_string_dec a b : Reflect (string_dec a b) (a = b) (a <> b).
+Global Instance Reflect_string_dec a b : Reflect (String.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using string_dec_sound.
+  apply iff_to_reflect; auto using String.eqb_eq.
 Qed.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use String.compare instead.")] *)
-Fixpoint string_cmp (l r : string) : comparison :=
+Fixpoint deprecated_string_cmp (l r : string) : comparison :=
   match l , r with
     | EmptyString , EmptyString => Eq
     | EmptyString , _ => Lt
     | _ , EmptyString => Gt
     | String l ls , String r rs =>
-      ascii_cmp l r >> string_cmp ls rs
+      ascii_cmp l r >> deprecated_string_cmp ls rs
   end.
 
+#[deprecated(since="8.15",note="Use String.compare instead.")]
+Notation string_cmp := deprecated_string_cmp.
+
 Section Program_Scope.
   Variable modulus : nat.
   Hypothesis one_lt_mod : 1 < modulus.

theories/Programming/Extras.v

@@ -23,43 +23,57 @@ Module FunNotation.
 End FunNotation.
 Import FunNotation.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
-Definition uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.
+Definition deprecated_uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
-Definition curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation uncurry := deprecated_uncurry.
 
-Lemma uncurry_curry : forall A B C (f : A -> B -> C) a b,
+Definition deprecated_curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).
+
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation curry := deprecated_curry.
+
+Lemma deprecated_uncurry_curry : forall A B C (f : A -> B -> C) a b,
     curry (uncurry f) a b = f a b.
 Proof.
   unfold curry, uncurry.
   reflexivity.
 Qed.
 
-Lemma curry_uncurry : forall A B C (f : A * B -> C) ab,
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation uncurry_curry := deprecated_uncurry_curry.
+
+Lemma deprecated_curry_uncurry : forall A B C (f : A * B -> C) ab,
     uncurry (curry f) ab = f ab.
 Proof.
   unfold uncurry, curry.
   destruct ab.
   reflexivity.
 Qed.
 
-Fixpoint zip A B (xs:list A) (ys:list B) : list (A * B) :=
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation curry_uncurry := deprecated_curry_uncurry.
+
+Fixpoint deprecated_zip A B (xs:list A) (ys:list B) : list (A * B) :=
   match xs, ys with
   | [], _ => []
   | _, [] => []
-  | x::xs, y::ys => (x,y)::zip xs ys
+  | x::xs, y::ys => (x,y)::deprecated_zip xs ys
   end
 .
 
-Fixpoint unzip A B (xys:list (A * B)) : list A * list B :=
+#[deprecated(note = "Use List.combine instead.")]
+Notation zip := deprecated_zip.
+
+Fixpoint deprecated_unzip A B (xys:list (A * B)) : list A * list B :=
 match xys with
 | [] => ([], [])
-| (x,y)::xys => let (xs,ys) := unzip xys in (x::xs,y::ys)
+| (x,y)::xys => let (xs,ys) := deprecated_unzip xys in (x::xs,y::ys)
 end.
 
+#[deprecated(note = "Use List.split instead.")]
+Notation unzip := deprecated_unzip.
+
 Definition sum_tot {A} (x:A + A) : A := match x with inl a => a | inr a => a end.
 
 Definition forEach A B (xs:list A) (f:A -> B) : list B := map f xs.