From 620b66fff543a29d7b8ca4fd7048396b4ef1d323 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Oct 2020 11:00:33 +0200
Subject: [PATCH] declare scopes before using them

---
 _CoqProject        | 2 --
 theories/base.v    | 1 +
 theories/binders.v | 4 +++-
 theories/fin.v     | 1 +
 theories/numbers.v | 6 ++++--
 theories/streams.v | 8 +++++---
 6 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index a90e9b51..77e45b94 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,4 @@
 -Q theories stdpp
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/options.v
 theories/base.v
diff --git a/theories/base.v b/theories/base.v
index 603fe11a..ceb16eef 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -183,6 +183,7 @@ Definition tc_to_bool (P : Prop)
 
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
+Declare Scope stdpp_scope.
 Delimit Scope stdpp_scope with stdpp.
 Global Open Scope stdpp_scope.
 
diff --git a/theories/binders.v b/theories/binders.v
index ce03ccd9..b2d2f4f9 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -12,9 +12,11 @@ From stdpp Require Import options.
 (* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
+Declare Scope binder_scope.
+Delimit Scope binder_scope with binder.
+
 Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
-Delimit Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
 Instance binder_dec_eq : EqDecision binder.
diff --git a/theories/fin.v b/theories/fin.v
index dc99e703..5e72506b 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -15,6 +15,7 @@ ambiguity. *)
 Notation fin := Fin.t.
 Notation FS := Fin.FS.
 
+Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
 Arguments Fin.FS _ _%fin : assert.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 3976a72b..420c82d4 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -658,13 +658,15 @@ Qed.
 Local Close Scope Qc_scope.
 
 (** * Positive rationals *)
+Declare Scope Qp_scope.
+Delimit Scope Qp_scope with Qp.
+
 (** The theory of positive rationals is very incomplete. We merely provide
 some operations and theorems that are relevant for fractional permissions. *)
 Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
 Hint Resolve Qp_prf : core.
-Delimit Scope Qp_scope with Qp.
-Bind Scope Qp_scope with Qp.
 Arguments Qp_car _%Qp : assert.
+Bind Scope Qp_scope with Qp.
 
 Local Open Scope Qc_scope.
 Local Open Scope Qp_scope.
diff --git a/theories/streams.v b/theories/streams.v
index 7022bfba..50c219c8 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,12 +1,14 @@
 From stdpp Require Export tactics.
 From stdpp Require Import options.
 
-CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
-Arguments scons {_} _ _ : assert.
+Declare Scope stream_scope.
 Delimit Scope stream_scope with stream.
-Bind Scope stream_scope with stream.
 Open Scope stream_scope.
+
+CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
+Arguments scons {_} _ _ : assert.
 Infix ":.:" := scons (at level 60, right associativity) : stream_scope.
+Bind Scope stream_scope with stream.
 
 Definition shead {A} (s : stream A) : A := match s with x :.: _ => x end.
 Definition stail {A} (s : stream A) : stream A := match s with _ :.: s => s end.
-- 
GitLab