Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)

.github/workflows/docker-action.yml

@@ -19,8 +19,13 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.16'
           - 'mathcomp/mathcomp-dev:coq-8.17'
+          - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:

README.md

@@ -24,9 +24,9 @@ which will be used to subsume notations for finite sets, eventually.
   - Cyril Cohen (initial)
   - Kazuhiko Sakaguchi
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.13 to 8.16
+- Compatible Coq versions: Coq 8.16 to 8.18
 - Additional dependencies:
-  - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
+  - [MathComp ssreflect 2.0 to 2.1](https://math-comp.github.io)
 - Coq namespace: `mathcomp.finmap`
 - Related publication(s): none
 

coq-mathcomp-finmap.opam

@@ -21,8 +21,8 @@ which will be used to subsume notations for finite sets, eventually."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.16" & < "8.18~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.1~") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.19~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.0" & < "2.2~") | (= "dev") }
 ]
 
 tags: [

finmap.v

@@ -3,7 +3,7 @@
 
 From HB Require Import structures.
 Set Warnings "-notation-incompatible-format".
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
 Set Warnings "notation-incompatible-format".
 From mathcomp Require Import choice path finset finfun fintype bigop.
 
@@ -2919,16 +2919,16 @@
 Arguments ffun_of_fmap : simpl never.
 
 Notation "[ 'fmap' x : aT => F ]" := (FinMap [ffun x : aT => F])
-  (at level 0, x name, only parsing) : fun_scope.
+  (at level 0, x name, only parsing) : function_scope.
 
 Notation "[ 'fmap' : aT => F ]" := (FinMap [ffun _ : aT => F])
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fmap' x => F ]" := [fmap x : _ => F]
-  (at level 0, x name, format "[ 'fmap'  x  =>  F ]") : fun_scope.
+  (at level 0, x name, format "[ 'fmap'  x  =>  F ]") : function_scope.
 
 Notation "[ 'fmap' => F ]" := [fmap: _ => F]
-  (at level 0, format "[ 'fmap' =>  F ]") : fun_scope.
+  (at level 0, format "[ 'fmap' =>  F ]") : function_scope.
 
 Canonical finmap_of_finfun (K : choiceType) V (A : {fset K}) (f : {ffun A -> V}) := FinMap f.
 Arguments finmap_of_finfun /.
@@ -3794,101 +3794,101 @@
 
 Notation "[ 'fsfun[' key ] x : aT => F | default ]" :=
   (fsfun_of_ffun key (fun x : aT => F) (fun x => default))
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x : aT => F | default ]" :=
   [fsfun[fsfun_key] x : aT => F | default]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] x : aT => F ]" := [fsfun[key] x : aT => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x : aT => F ]" := [fsfun x : aT => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] x => F | default ]" :=
   [fsfun[key] x : _ => F | default ]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x => F | default ]" := [fsfun x : _ => F | default]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] x => F ]" := [fsfun[key] x => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x => F ]" := [fsfun x => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ]=> F | default ]" :=
   [fsfun[key] _ => F | default ]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun=>' F | default ]" := [fsfun _ => F | default]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ]=> F ]" := [fsfun[key]=> F | _]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun=>' F ]" := [fsfun=> F | _]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Definition fsfun_of_fun key (K : choiceType) (V : eqType)
    (S : {fset K}) (h : K -> V) default :=
   [fsfun[key] x : S => h (val x) | default x].
 
 Notation "[ 'fsfun[' key ] x 'in' S => F | default ]" :=
   (fsfun_of_fun key S (fun x => F) (fun x => default))
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x 'in' S => F | default ]" :=
   [fsfun[fsfun_key] x in S => F | default]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] x 'in' S => F ]" :=
   [fsfun[key] x in S => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' x 'in' S => F ]" :=
   [fsfun[fsfun_key] x in S => F | _]
-  (at level 0, x at level 99, only parsing) : fun_scope.
+  (at level 0, x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] 'in' S => F | default ]" :=
   [fsfun[key] _ in S => F | default]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun' 'in' S => F | default ]" :=
   [fsfun[fsfun_key] in S => F | default]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun[' key ] 'in' S => F ]" :=
   [fsfun[key] in S => F | _]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun' 'in' S => F ]" :=
   [fsfun[fsfun_key] in S => F | _]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 (* only printing *)
 Notation "[ 'fs' 'fun' x : aT => F ]" := [fsfun[_] x : aT => F]
   (at level 0, x at level 99,
-  format "[ 'fs' 'fun'  x  :  aT  =>  F ]") : fun_scope.
+  format "[ 'fs' 'fun'  x  :  aT  =>  F ]") : function_scope.
 
 Notation "[ 'fs' 'fun' x 'in' aT => F ]" := [fsfun[_] x in aT => F]
   (at level 0, x at level 99,
-  format "[ 'fs' 'fun'  x  'in'  aT  =>  F ]") : fun_scope.
+  format "[ 'fs' 'fun'  x  'in'  aT  =>  F ]") : function_scope.
 
 Fact fsfun0_key : unit. Proof. exact: tt. Qed.
 Notation "[ 'fsfun' 'for' default ]" := (fsfun_of_ffun fsfun0_key [fmap] default)
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun' 'of' x => default ]" := [fsfun for fun x => default]
-  (at level 0,  x at level 99, only parsing) : fun_scope.
+  (at level 0,  x at level 99, only parsing) : function_scope.
 
 Notation "[ 'fsfun' 'with' default ]" := [fsfun of _ => default]
-  (at level 0, only parsing) : fun_scope.
+  (at level 0, only parsing) : function_scope.
 
 Notation "[ 'fsfun' ]" := [fsfun for _]
- (at level 0, format "[ 'fsfun' ]") : fun_scope.
+ (at level 0, format "[ 'fsfun' ]") : function_scope.
 
 Section FsfunTheory.
 Variables (key : unit) (K : choiceType) (V : eqType) (default : K -> V).
@@ -3946,12 +3946,12 @@
 Notation "[ 'fsfun' f 'with' d1 , .. , dn ]" :=
   (app_fsdelta d1%FUN_DELTA .. (app_fsdelta dn%FUN_DELTA f) ..)
   (at level 0, f at level 99, format
-  "'[hv' [ '[' 'fsfun' '/ '  f ']' '/'  'with'  '[' d1 , '/'  .. , '/'  dn ']' ] ']'") : fun_scope.
+  "'[hv' [ '[' 'fsfun' '/ '  f ']' '/'  'with'  '[' d1 , '/'  .. , '/'  dn ']' ] ']'") : function_scope.
 
 Notation "[ 'fsfun' f 'without' x1 , .. , xn ]" :=
   (app_fswithout x1 .. (app_fswithout xn f) ..)
   (at level 0, f at level 99, format
-  "'[hv' [ '[' 'fsfun' '/ '  f ']' '/'  'without'  '[' x1 , '/'  .. , '/'  xn ']' ] ']'") : fun_scope.
+  "'[hv' [ '[' 'fsfun' '/ '  f ']' '/'  'without'  '[' x1 , '/'  .. , '/'  xn ']' ] ']'") : function_scope.
 
 Section FsWithTheory.
 Variables (K : choiceType) (V : eqType) (default : K -> V).

meta.yml

@@ -31,47 +31,37 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.13 to 8.16
-  opam: '{ (>= "8.13" & < "8.17~") | (= "dev") }'
+  text: Coq 8.16 to 8.18
+  opam: '{ (>= "8.16" & < "8.19~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.13'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
+- version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
+- version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: 'coq-8.13'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
+- version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
+- version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.16'
+- version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
+    version: '{ (>= "2.0" & < "2.2~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
+    [MathComp ssreflect 2.0 to 2.1](https://math-comp.github.io)
 
 namespace: mathcomp.finmap