Adapt to rocq-prover/rocq#21849

Author: proux01

.github/workflows/coq-docker.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ '8.18', '8.19', '8.20' , '9.0' , '9.1' ]
+        coq-version: [ '8.19', '8.20' , '9.0' , '9.1' ]
         extra-gh-reportify: [ '' ]
         skip-validate: [ '' ]
         include:

.github/workflows/coq-opam-package.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: ['dev', '8.20.0', '8.19.0', '8.18.0' , '9.0.0' , '9.1.0' ]
+        coq-version: ['dev', '8.20.0', '8.19.0', '9.0.0' , '9.1.0' ]
         os: [{name: 'Ubuntu',
               runs-on: 'ubuntu-latest',
               ocaml-compiler: '4.14.0',

src/Rewriter/Language/Language.v

@@ -296,7 +296,7 @@ Module Compilers.
   Declare Scope etype_scope.
   Delimit Scope etype_scope with etype.
   Bind Scope etype_scope with type.type.
-  Global Arguments type.base {_} _%etype.
+  Global Arguments type.base {_} _%_etype.
   Infix "->" := type.arrow : etype_scope.
   Infix "==" := type.eqv : type_scope.
   Module base.
@@ -911,7 +911,7 @@ Module Compilers.
     Module Export Notations.
       Declare Scope ident_scope.
       Delimit Scope ident_scope with ident.
-      Global Arguments expr.Ident {base_type%type ident%function var%function t%etype} idc%ident.
+      Global Arguments expr.Ident {base_type%_type ident%_function var%_function t%_etype} idc%_ident.
       Notation "# x" := (expr.Ident x) (only parsing) : expr_pat_scope.
       Notation "# x" := (@expr.Ident _ _ _ _ x) : expr_scope.
       Notation "x @ y" := (expr.App x%expr_pat y%expr_pat) (only parsing) : expr_pat_scope.

src/Rewriter/Rewriter/Rewriter.v

@@ -358,7 +358,7 @@ Module Compilers.
       | App (f x : pattern).
     End Raw.
 
-    Global Arguments Wildcard {base ident}%type t%ptype.
+    Global Arguments Wildcard {base ident}%_type t%_ptype.
 
     Fixpoint to_raw {base ident raw_ident}
              {to_raw_ident : forall t, ident t -> raw_ident}

src/Rewriter/Util/Decidable.v

@@ -11,7 +11,7 @@ From Coq Require Import BinNat.
 Local Open Scope type_scope.
 
 Class Decidable (P : Prop) := dec : {P} + {~P}.
-Arguments dec _%type_scope {_}.
+Arguments dec _%_type_scope {_}.
 Notation DecidableRel R := (forall x y, Decidable (R x y)).
 
 Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10.