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

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

4 files changed, 17 insertions, 6 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1e6843d511..76c39f275d 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -37,8 +37,8 @@ Inductive bool : Set :=
 
 Add Printing If bool.
 
+Declare Scope bool_scope.
 Delimit Scope bool_scope with bool.
-
 Bind Scope bool_scope with bool.
 
 (** Basic boolean operators *)
@@ -136,6 +136,7 @@ Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.
 
+Declare Scope nat_scope.
 Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
 Arguments S _%nat.
@@ -228,10 +229,13 @@ Inductive list (A : Type) : Type :=
 
 Arguments nil {A}.
 Arguments cons {A} a l.
-Infix "::" := cons (at level 60, right associativity) : list_scope.
+
+Declare Scope list_scope.
 Delimit Scope list_scope with list.
 Bind Scope list_scope with list.
 
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+
 Local Open Scope list_scope.
 
 Definition length (A : Type) : list A -> nat :=
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 1ff00ec11c..537400fb05 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,8 +42,11 @@ Notation zero := (D0 Nil).
 
 Inductive int := Pos (d:uint) | Neg (d:uint).
 
+Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
+
+Declare Scope dec_int_scope.
 Delimit Scope dec_int_scope with int.
 Bind Scope dec_int_scope with int.
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 72073bb4f6..8f8e639187 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -108,13 +108,17 @@ End IfNotations.
 
 (** Scopes *)
 
-Delimit Scope type_scope with type.
-Delimit Scope function_scope with function.
+Declare Scope core_scope.
 Delimit Scope core_scope with core.
 
-Bind Scope type_scope with Sortclass.
+Declare Scope function_scope.
+Delimit Scope function_scope with function.
 Bind Scope function_scope with Funclass.
 
+Declare Scope type_scope.
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
+
 Open Scope core_scope.
 Open Scope function_scope.
 Open Scope type_scope.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index b6afba29a0..db8857df64 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -697,7 +697,7 @@ End Choice_lemmas.
 
 Section Dependent_choice_lemmas.
 
-  Variables X : Set.
+  Variable X : Set.
   Variable R : X -> X -> Prop.
 
   Lemma dependent_choice :