Merge pull request #17 from coq-community/function_scope

Update CI and fix notation scopes

.github/workflows/docker-action.yml

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

meta.yml

@@ -78,10 +78,20 @@ dependencies:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.18'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
+- version: '2.1.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.16'

theories/sets/sset1.v

@@ -2065,7 +2065,7 @@ Definition allf (g: Set) (p: property) :=
    forall x, inc x (domain g) -> (p (Vg g x)).
 
 Notation "f1 =1g f2" := (same_Vg f1 f2)
-  (at level 70, no associativity) : fun_scope.
+  (at level 70, no associativity) : type_scope.
 
 (** The function [V] is well-defined for functional graphs. 
 Here are some properties  *)

theories/sets/sset2.v

@@ -786,7 +786,7 @@ Definition cstgp (f E: Set) := singl_val_fp (inc ^~E) (Vg f).
 
 
 Notation "f1 =1f f2" := (same_Vf f1 f2)
-  (at level 70, no associativity) : fun_scope.
+  (at level 70, no associativity) : type_scope.
 
 Lemma function_exten3 f g:
   function f -> function g ->