Adapt to math-comp/math-comp#1354

Author: proux01

README.md

@@ -41,9 +41,9 @@ remains the sole trusted code base.
   - Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi))
   - Kazuhiko Sakaguchi ([**@pi8027**](https://github.com/pi8027))
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: 8.16 or later
+- Compatible Coq versions: 8.18 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
   - [CoqEAL 2.0.4 or later](https://github.com/coq-community/coqeal)

coq-mathcomp-apery.opam

@@ -23,7 +23,7 @@ remains the sole trusted code base."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
+  "coq" {(>= "8.18" & < "9.1~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "2.3" & < "2.4~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 

meta.yml

@@ -51,8 +51,8 @@ license:
   identifier: CECILL-C
 
 supported_coq_versions:
-  text: 8.16 or later
-  opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
+  text: 8.18 or later
+  opam: '{(>= "8.18" & < "9.1~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: '2.3.0-coq-8.20'

theories/multinomial.v

@@ -18,8 +18,7 @@ Definition multinomial (l : seq nat) : nat :=
 Arguments multinomial l : simpl never.
 
 (* Notation under evaluation ... *)
-Notation "''C' [ l ]" := (multinomial l)
-  (at level 8, format "''C' [ l ]") : nat_scope.
+Notation "''C' [ l ]" := (multinomial l) : nat_scope.
 
 (* For instance I would like to avoid double brackets, like in: *)
 Check 'C[[::]].