Remove deprecated definitions

Author: liyishuai

.github/workflows/docker-action.yml

@@ -25,6 +25,7 @@ jobs:
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:

meta.yml

@@ -40,6 +40,7 @@ tested_coq_opam_versions:
   - version: '8.15'
   - version: '8.16'
   - version: '8.17'
+  - version: '8.18'
   - version: 'dev'
 
 make_target: theories

theories/Data/Char.v

@@ -6,45 +6,6 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-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 =>
-      if Bool.eqb l1 r1 then
-      if Bool.eqb l2 r2 then
-      if Bool.eqb l3 r3 then
-      if Bool.eqb l4 r4 then
-      if Bool.eqb l5 r5 then
-      if Bool.eqb l6 r6 then
-      if Bool.eqb l7 r7 then
-      if Bool.eqb l8 r8 then true
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-  end.
-
-#[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.
-  destruct l; destruct r.
-  repeat match goal with
-           | [ |- (if ?X then _ else _) = true <-> _ ] =>
-             consider X; intros; subst
-         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.eqb }.
 

theories/Data/String.v

@@ -39,30 +39,6 @@ Definition deprecated_ascii_cmp (l r : Ascii.ascii) : comparison :=
 #[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.eqb l r then deprecated_string_dec ls rs
-      else false
-    | _ , _ => false
-  end.
-
-#[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; 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.eqb |}.