declare scopes before using them

_CoqProject

 -Q theories stdpp
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/options.v
 theories/base.v

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.
 

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.

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.
 

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.

theories/streams.v

 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.