Don't ignore undeclared-scope warnings

.travis.yml

@@ -42,21 +42,15 @@ matrix:
   - env:
     - COQ=8.10
     <<: *NIX
-  - env:
-    - COQ=8.9
-    <<: *NIX
-  - env:
-    - COQ=8.8
-    <<: *NIX
 
   # Test supported versions of Coq via OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:dev
+    - COQ_IMAGE=coqorg/coq:8.11
     - PACKAGE=coq-lemma-overloading.dev
     - NJOBS=2
     <<: *OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:8.11
+    - COQ_IMAGE=coqorg/coq:dev
     - PACKAGE=coq-lemma-overloading.dev
     - NJOBS=2
     <<: *OPAM

README.md

@@ -45,8 +45,8 @@ re-implementations for comparison.
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU General Public License v3.0 or later](LICENSE.md)
-- Compatible Coq versions: 8.8 or later (use releases for other Coq versions)
-- Additional Coq dependencies:
+- Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
+- Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.7.0 or later (`ssreflect` suffices)
 - Coq namespace: `LemmaOverloading`
 - Related publication(s):

_CoqProject

@@ -4,7 +4,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
--arg -w -arg -undeclared-scope
 
 theories/prelude.v
 theories/rels.v

coq-lemma-overloading.opam

@@ -22,8 +22,7 @@ re-implementations for comparison."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "ocaml"
-  "coq" {(>= "8.8" & < "8.12~") | (= "dev")}
+  "coq" {(>= "8.10" & < "8.12~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.11~") | (= "dev")}
 ]
 

meta.yml

@@ -55,17 +55,15 @@ license:
   file: LICENSE.md
 
 supported_coq_versions:
-  text: 8.8 or later (use releases for other Coq versions)
-  opam: '{(>= "8.8" & < "8.12~") | (= "dev")}'
+  text: 8.10 or later (use releases for other Coq versions)
+  opam: '{(>= "8.10" & < "8.12~") | (= "dev")}'
 
 tested_coq_nix_versions:
 - version_or_url: '8.10'
-- version_or_url: '8.9'
-- version_or_url: '8.8'
 
 tested_coq_opam_versions:
-- version: dev
 - version: '8.11'
+- version: dev
 
 dependencies:
 - opam:

theories/rels.v

@@ -34,6 +34,7 @@ Lemma orpT p : p \/ True <-> True.    Proof. by intuition. Qed.
 Lemma orFp p : False \/ p <-> p.      Proof. by intuition. Qed.
 Lemma orpF p : p \/ False <-> p.      Proof. by intuition. Qed.
 
+Declare Scope rel_scope.
 Delimit Scope rel_scope with rel.
 Open Scope rel_scope.
 

theories/stsep.v

@@ -23,6 +23,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope stsep_scope.
 Delimit Scope stsep_scope with stsep.
 Open Scope stsep_scope.