Adapting standard library to the introduction of "Declare Scope".

Removing in passing two Local which are no-ops in practice.

5 files changed, 8 insertions, 0 deletions

diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index 03e611f549..c376efef2e 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : crelation A := R.
 (** Overloaded notations for setoid equivalence and inequivalence.
     Not to be confused with [eq] and [=]. *)
 
+Declare Scope equiv_scope.
+
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 09b35ca75d..97510578ae 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -87,6 +87,7 @@ Hint Extern 2 (ProperProxy ?R _) =>
   not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
+Declare Scope signature_scope.
 Delimit Scope signature_scope with signature.
 
 Module ProperNotations.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5217aedb88..516ea12099 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : relation A := R.
 (** Overloaded notations for setoid equivalence and inequivalence.
     Not to be confused with [eq] and [=]. *)
 
+Declare Scope equiv_scope.
+
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 1858ba76ae..001b7dfdfd 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -88,6 +88,7 @@ Hint Extern 2 (ProperProxy ?R _) =>
   not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
+Declare Scope signature_scope.
 Delimit Scope signature_scope with signature.
 
 Module ProperNotations.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 2ab3af2029..86a3a88be9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -357,6 +357,8 @@ Definition predicate_implication {l : Tlist} :=
 
 (** Notations for pointwise equivalence and implication of predicates. *)
 
+Declare Scope predicate_scope.
+
 Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
 Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.