From 3b7a6761f5c9bf5026c4517e8032aa4384185528 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Mar 2018 20:07:34 +0200
Subject: Adding a command "Declare Scope" and deprecating scope implicit
 declaration.

---
 interp/notation.ml       | 29 +++++++++++++++++++++-----
 interp/notation.mli      |  3 +++
 stm/vernac_classifier.ml |  3 ++-
 vernac/g_vernac.mlg      |  8 ++++++--
 vernac/metasyntax.ml     | 53 ++++++++++++++++++++++++++++++++++++------------
 vernac/metasyntax.mli    |  3 ++-
 vernac/ppvernac.ml       |  4 ++++
 vernac/vernacentries.ml  |  4 ++++
 vernac/vernacexpr.ml     |  1 +
 9 files changed, 86 insertions(+), 22 deletions(-)

diff --git a/interp/notation.ml b/interp/notation.ml
index 55ead946cb..6b26f66100 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -98,21 +98,40 @@ let init_scope_map () =
 (**********************************************************************)
 (* Operations on scopes *)
 
+let warn_undeclared_scope =
+  CWarnings.create ~name:"undeclared-scope" ~category:"deprecated"
+                   (fun (scope) ->
+                    strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit "
+                    ++ str "\"Declare Scope " ++ str scope ++ str ".\".")
+
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
   with Not_found ->
-(*    Flags.if_warn message ("Creating scope "^scope);*)
     scope_map := String.Map.add scope empty_scope !scope_map
 
 let error_unknown_scope sc =
   user_err ~hdr:"Notation"
     (str "Scope " ++ str sc ++ str " is not declared.")
 
-let find_scope scope =
+let find_scope ?(tolerant=false) scope =
   try String.Map.find scope !scope_map
-  with Not_found -> error_unknown_scope scope
+  with Not_found ->
+    if tolerant then
+      (* tolerant mode to be turn off after deprecation phase *)
+      begin
+        warn_undeclared_scope scope;
+        scope_map := String.Map.add scope empty_scope !scope_map;
+        empty_scope
+      end
+    else
+      error_unknown_scope scope
+
+let check_scope ?(tolerant=false) scope =
+  let _ = find_scope ~tolerant scope in ()
+
+let ensure_scope scope = check_scope ~tolerant:true scope
 
-let check_scope sc = let _ = find_scope sc in ()
+let find_scope scope = find_scope scope
 
 (* [sc] might be here a [scope_name] or a [delimiter]
    (now allowed after Open Scope) *)
@@ -418,7 +437,7 @@ type prim_token_infos = {
 let cache_prim_token_interpretation (_,infos) =
   let sc = infos.pt_scope in
   let uid = infos.pt_uid in
-  declare_scope sc;
+  check_scope ~tolerant:true sc;
   prim_token_interp_infos :=
     String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
   List.iter (fun r -> prim_token_uninterp_infos :=
diff --git a/interp/notation.mli b/interp/notation.mli
index e5478eff48..6e59c0fd70 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *)
 
 val declare_scope : scope_name -> unit
 
+(* To be removed after deprecation phase *)
+val ensure_scope : scope_name -> unit
+
 val current_scopes : unit -> scopes
 
 (** Check where a scope is opened or not in a scope list, or in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2170477938..85babd922b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -168,7 +168,8 @@ let classify_vernac e =
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
-    | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+    | VernacOpenCloseScope _ | VernacDeclareScope _
+    | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74516e320c..44c0159d1b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram
 	 info = hint_info ->
 	   { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
 
+      (* Should be in syntax, but camlp5 would not factorize *)
+      | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
+          { VernacDeclareScope sc }
+
       (* System directory *)
       | IDENT "Pwd" -> { VernacChdir None }
       | IDENT "Cd" -> { VernacChdir None }
@@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
          -> { VernacSyntaxExtension (false, (s,l)) }
 
-     (* "Print" "Grammar" should be here but is in "command" entry in order
-        to factorize with other "Print"-based vernac entries *)
+     (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
+        to factorize with other "Print"-based or "Declare"-based vernac entries *)
   ] ]
   ;
   only_parsing:
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d66a121437..1f36b042fe 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1306,8 +1306,18 @@ type notation_obj = {
   notobj_notation : notation * notation_location;
 }
 
-let load_notation _ (_, nobj) =
-  Option.iter Notation.declare_scope nobj.notobj_scope
+let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
+  (* When the default shall be to require that a scope already exists *)
+  (* the call to ensure_scope will have to be removed *)
+  if silently_define_scope_if_undefined then
+    (* Don't warn if the scope is not defined: *)
+    (* there was already a warning at "cache" time *)
+    Option.iter Notation.declare_scope nobj.notobj_scope
+  else
+    Option.iter Notation.ensure_scope nobj.notobj_scope
+
+let load_notation =
+  load_notation_common true
 
 let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
@@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) =
   end
 
 let cache_notation o =
-  load_notation 1 o;
+  load_notation_common false 1 o;
   open_notation 1 o
 
 let subst_notation (subst, nobj) =
@@ -1566,25 +1576,39 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   add_notation local env c (df,modifiers) sc
 
 (**********************************************************************)
-(* Delimiters and classes bound to scopes                             *)
+(* Scopes, delimiters and classes bound to scopes                     *)
 
 type scope_command =
-  | ScopeDelim of string
+  | ScopeDeclare
+  | ScopeDelimAdd of string
+  | ScopeDelimRemove
   | ScopeClasses of scope_class list
-  | ScopeRemove
 
-let load_scope_command _ (_,(scope,dlm)) =
-  Notation.declare_scope scope
+let load_scope_command_common silently_define_scope_if_undefined _ (_,(scope,o)) =
+  let declare_scope_if_needed =
+    if silently_define_scope_if_undefined then Notation.declare_scope
+    else Notation.ensure_scope in
+  match o with
+  | ScopeDeclare -> Notation.declare_scope scope
+  (* When the default shall be to require that a scope already exists *)
+  (* the call to declare_scope_if_needed will have to be removed below *)
+  | ScopeDelimAdd dlm -> declare_scope_if_needed scope
+  | ScopeDelimRemove -> declare_scope_if_needed scope
+  | ScopeClasses cl -> declare_scope_if_needed scope
+
+let load_scope_command =
+  load_scope_command_common true
 
 let open_scope_command i (_,(scope,o)) =
   if Int.equal i 1 then
     match o with
-    | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+    | ScopeDeclare -> ()
+    | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm
+    | ScopeDelimRemove -> Notation.remove_delimiters scope
     | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
-    | ScopeRemove -> Notation.remove_delimiters scope
 
 let cache_scope_command o =
-  load_scope_command 1 o;
+  load_scope_command_common false 1 o;
   open_scope_command 1 o
 
 let subst_scope_command (subst,(scope,o as x)) = match o with
@@ -1604,11 +1628,14 @@ let inScopeCommand : scope_name * scope_command -> obj =
       subst_function = subst_scope_command;
       classify_function = (fun obj -> Substitute obj)}
 
+let declare_scope scope =
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDeclare))
+
 let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimAdd key))
 
 let remove_delimiters scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimRemove))
 
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 73bee7121b..7a74dcfaa9 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -27,8 +27,9 @@ val add_notation : locality_flag -> env -> constr_expr ->
 
 val add_notation_extra_printing_rule : string -> string -> string -> unit
 
-(** Declaring delimiter keys and default scopes *)
+(** Declaring scopes, delimiter keys and default scopes *)
 
+val declare_scope : scope_name -> unit
 val add_delimiters : scope_name -> string -> unit
 val remove_delimiters : scope_name -> unit
 val add_class_scope : scope_name -> scope_class list -> unit
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 93e4e89a12..63e9e4fe49 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -635,6 +635,10 @@ open Pputils
           keyword (if opening then "Open " else "Close ") ++
             keyword "Scope" ++ spc() ++ str sc
         )
+      | VernacDeclareScope sc ->
+        return (
+          keyword "Declare Scope" ++ spc () ++ str sc
+        )
       | VernacDelimiters (sc,Some key) ->
         return (
           keyword "Delimit Scope" ++ spc () ++ str sc ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f7ba305374..0fccfd22c6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -408,6 +408,9 @@ let vernac_syntax_extension atts infix l =
   if infix then Metasyntax.check_infix_modifiers (snd l);
   Metasyntax.add_syntax_extension local l
 
+let vernac_declare_scope sc =
+  Metasyntax.declare_scope sc
+
 let vernac_delimiters sc = function
   | Some lr -> Metasyntax.add_delimiters sc lr
   | None -> Metasyntax.remove_delimiters sc
@@ -2094,6 +2097,7 @@ let interp ?proof ~atts ~st c =
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
       vernac_syntax_extension atts infix sl
+  | VernacDeclareScope sc -> vernac_declare_scope sc
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8fb74e6d78..11b2a7d802 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -325,6 +325,7 @@ type nonrec vernac_expr =
   (* Syntax *)
   | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of bool * scope_name
+  | VernacDeclareScope of scope_name
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacInfix of (lstring * syntax_modifier list) *
-- 
cgit v1.2.3


From 8e675d70ad1f60cbbf9f1e630ce6dee61347c7ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Jul 2018 12:32:35 +0200
Subject: Support for Local flag in Declare Scope, Undelimit/Delimit Scope,
 Bind Scope.

This is for use in modules. By default, the behavior is local in
sections and Global is forbidden in sections. By default, the behavior
is global in modules.
---
 vernac/metasyntax.ml    | 31 +++++++++++++++++--------------
 vernac/metasyntax.mli   |  8 ++++----
 vernac/vernacentries.ml | 29 +++++++++++++++++------------
 3 files changed, 38 insertions(+), 30 deletions(-)

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 1f36b042fe..2e5e11bb09 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1584,7 +1584,7 @@ type scope_command =
   | ScopeDelimRemove
   | ScopeClasses of scope_class list
 
-let load_scope_command_common silently_define_scope_if_undefined _ (_,(scope,o)) =
+let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) =
   let declare_scope_if_needed =
     if silently_define_scope_if_undefined then Notation.declare_scope
     else Notation.ensure_scope in
@@ -1599,7 +1599,7 @@ let load_scope_command_common silently_define_scope_if_undefined _ (_,(scope,o))
 let load_scope_command =
   load_scope_command_common true
 
-let open_scope_command i (_,(scope,o)) =
+let open_scope_command i (_,(local,scope,o)) =
   if Int.equal i 1 then
     match o with
     | ScopeDeclare -> ()
@@ -1611,34 +1611,37 @@ let cache_scope_command o =
   load_scope_command_common false 1 o;
   open_scope_command 1 o
 
-let subst_scope_command (subst,(scope,o as x)) = match o with
+let subst_scope_command (subst,(local,scope,o as x)) = match o with
   | ScopeClasses cl ->
       let cl' = List.map_filter (subst_scope_class subst) cl in
       let cl' =
         if List.for_all2eq (==) cl cl' then cl
         else cl' in
-      scope, ScopeClasses cl'
+      local, scope, ScopeClasses cl'
   | _ -> x
 
-let inScopeCommand : scope_name * scope_command -> obj =
+let classify_scope_command (local, _, _ as o) =
+  if local then Dispose else Substitute o
+
+let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
   declare_object {(default_object "DELIMITERS") with
       cache_function = cache_scope_command;
       open_function = open_scope_command;
       load_function = load_scope_command;
       subst_function = subst_scope_command;
-      classify_function = (fun obj -> Substitute obj)}
+      classify_function = classify_scope_command}
 
-let declare_scope scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDeclare))
+let declare_scope local scope =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare))
 
-let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimAdd key))
+let add_delimiters local scope key =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key))
 
-let remove_delimiters scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimRemove))
+let remove_delimiters local scope =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove))
 
-let add_class_scope scope cl =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
+let add_class_scope local scope cl =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
 
 (* Check if abbreviation to a name and avoid early insertion of
    maximal implicit arguments *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 7a74dcfaa9..38dbdf7e41 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -29,10 +29,10 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit
 
 (** Declaring scopes, delimiter keys and default scopes *)
 
-val declare_scope : scope_name -> unit
-val add_delimiters : scope_name -> string -> unit
-val remove_delimiters : scope_name -> unit
-val add_class_scope : scope_name -> scope_class list -> unit
+val declare_scope : locality_flag -> scope_name -> unit
+val add_delimiters : locality_flag -> scope_name -> string -> unit
+val remove_delimiters : locality_flag -> scope_name -> unit
+val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
 
 (** Add only the interpretation of a notation that already has pa/pp rules *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0fccfd22c6..84ce79d402 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -403,20 +403,24 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension atts infix l =
+let vernac_syntax_extension ~atts infix l =
   let local = enforce_module_locality atts.locality in
   if infix then Metasyntax.check_infix_modifiers (snd l);
   Metasyntax.add_syntax_extension local l
 
-let vernac_declare_scope sc =
-  Metasyntax.declare_scope sc
+let vernac_declare_scope ~atts sc =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.declare_scope local sc
 
-let vernac_delimiters sc = function
-  | Some lr -> Metasyntax.add_delimiters sc lr
-  | None -> Metasyntax.remove_delimiters sc
+let vernac_delimiters ~atts sc action =
+  let local = enforce_module_locality atts.locality in
+  match action with
+  | Some lr -> Metasyntax.add_delimiters local sc lr
+  | None -> Metasyntax.remove_delimiters local sc
 
-let vernac_bind_scope sc cll =
-  Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
+let vernac_bind_scope ~atts sc cll =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll)
 
 let vernac_open_close_scope ~atts (b,s) =
   let local = enforce_section_locality atts.locality in
@@ -2096,10 +2100,10 @@ let interp ?proof ~atts ~st c =
 
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-      vernac_syntax_extension atts infix sl
-  | VernacDeclareScope sc -> vernac_declare_scope sc
-  | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
-  | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
+      vernac_syntax_extension ~atts infix sl
+  | VernacDeclareScope sc -> vernac_declare_scope ~atts sc
+  | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr
+  | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
   | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
   | VernacNotation (c,infpl,sc) ->
@@ -2236,6 +2240,7 @@ let check_vernac_supports_locality c l =
   | Some _, (
       VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+    | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacDeclareCustomEntry _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _
-- 
cgit v1.2.3


From 46ab3659dd1f2e4839064cfabc03bd19268fa44b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Mar 2018 14:47:06 +0200
Subject: Adapting standard library to the introduction of "Declare Scope".

Removing in passing two Local which are no-ops in practice.
---
 plugins/romega/ReflOmegaCore.v                |  2 ++
 plugins/setoid_ring/Field_theory.v            |  3 +++
 plugins/setoid_ring/Ncring_initial.v          |  5 +++--
 plugins/ssr/ssreflect.v                       |  3 +++
 plugins/ssr/ssrfun.v                          |  2 ++
 plugins/ssrmatching/ssrmatching.v             |  4 +++-
 test-suite/output/Arguments.v                 |  2 ++
 test-suite/output/Notations.v                 |  1 +
 theories/Bool/Bool.v                          |  2 ++
 theories/Classes/CEquivalence.v               |  2 ++
 theories/Classes/CMorphisms.v                 |  1 +
 theories/Classes/Equivalence.v                |  2 ++
 theories/Classes/Morphisms.v                  |  1 +
 theories/Classes/RelationClasses.v            |  2 ++
 theories/FSets/FMapAVL.v                      |  1 +
 theories/Init/Datatypes.v                     |  8 ++++++--
 theories/Init/Decimal.v                       |  3 +++
 theories/Init/Notations.v                     | 10 +++++++---
 theories/Init/Specif.v                        |  2 +-
 theories/MSets/MSetAVL.v                      |  2 ++
 theories/Numbers/BinNums.v                    |  3 +++
 theories/Numbers/Cyclic/Int31/Int31.v         |  1 +
 theories/Numbers/Integer/Abstract/ZDivEucl.v  |  1 +
 theories/Numbers/Integer/NatPairs/ZNatPairs.v |  6 +++++-
 theories/Numbers/NatInt/NZDomain.v            |  4 +++-
 theories/Program/Basics.v                     |  2 ++
 theories/Program/Utils.v                      |  5 +++--
 theories/QArith/QArith_base.v                 |  1 +
 theories/QArith/Qcanon.v                      |  1 +
 theories/Reals/Ranalysis1.v                   |  1 +
 theories/Reals/Raxioms.v                      |  1 +
 theories/Structures/OrdersFacts.v             |  1 +
 theories/Vectors/VectorDef.v                  |  1 +
 theories/ZArith/Int.v                         |  1 +
 34 files changed, 74 insertions(+), 13 deletions(-)

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 51b99b9935..da86f4274d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -8,6 +8,7 @@
  *************************************************************************)
 
 Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
+Declare Scope Int_scope.
 Delimit Scope Int_scope with I.
 
 (** * Abstract Integers. *)
@@ -716,6 +717,7 @@ Inductive term : Set :=
   | Topp : term -> term
   | Tvar : N -> term.
 
+Declare Scope romega_scope.
 Bind Scope romega_scope with term.
 Delimit Scope romega_scope with term.
 Arguments Tint _%I.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d9e32dbbf8..ce115f564f 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -19,6 +19,7 @@ Section MakeFieldPol.
 (* Field elements : R *)
 
 Variable R:Type.
+Declare Scope R_scope.
 Bind Scope R_scope with R.
 Delimit Scope R_scope with ring.
 Local Open Scope R_scope.
@@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth.
 (* Coefficients : C *)
 
 Variable C: Type.
+Declare Scope C_scope.
 Bind Scope C_scope with C.
 Delimit Scope C_scope with coef.
 
@@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N).
 
 (* Polynomial expressions : (PExpr C) *)
 
+Declare Scope PE_scope.
 Bind Scope PE_scope with PExpr.
 Delimit Scope PE_scope with poly.
 
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 523c7b02eb..1ca6227f25 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}.
   | Z0 => 0
   | Zneg p => -(gen_phiPOS p)
   end.
- Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
- Local Open Scope ZMORPHISM.
+ Declare Scope ZMORPHISM.
+ Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM.
+ Open Scope ZMORPHISM.
 
  Definition get_signZ z :=
   match z with
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b4144aa45e..460bdc6d23 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -86,6 +86,7 @@ Export SsrSyntax.
 (* recognize the expansion of the boolean if; using the default printer       *)
 (* avoids a spurrious trailing %GEN_IF.                                       *)
 
+Declare Scope general_if_scope.
 Delimit Scope general_if_scope with GEN_IF.
 
 Notation "'if' c 'then' v1 'else' v2" :=
@@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
 
 (* Force boolean interpretation of simple if expressions.                     *)
 
+Declare Scope boolean_if_scope.
 Delimit Scope boolean_if_scope with BOOL_IF.
 
 Notation "'if' c 'return' t 'then' v1 'else' v2" :=
@@ -125,6 +127,7 @@ Open Scope boolean_if_scope.
 (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *)
 (* Lists library) should be loaded before ssreflect so that their notations   *)
 (* do not mask all ssreflect forms.                                           *)
+Declare Scope form_scope.
 Delimit Scope form_scope with FORM.
 Open Scope form_scope.
 
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index b2d5143e36..99ff943e61 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -216,6 +216,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope fun_scope.
 Delimit Scope fun_scope with FUN.
 Open Scope fun_scope.
 
@@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y)
 Notation "@^~ x" := (fun f => f x)
   (at level 10, x at level 8, no associativity, format "@^~  x") : fun_scope.
 
+Declare Scope pair_scope.
 Delimit Scope pair_scope with PAIR.
 Open Scope pair_scope.
 
diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v
index 829ee05e11..9a53e1dd1a 100644
--- a/plugins/ssrmatching/ssrmatching.v
+++ b/plugins/ssrmatching/ssrmatching.v
@@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )"        (at level 0).
 Reserved Notation "( a 'in' b 'in' c )" (at level 0).
 Reserved Notation "( a 'as' b 'in' c )" (at level 0).
 
+Declare Scope ssrpatternscope.
+Delimit Scope ssrpatternscope with pattern.
+
 (* Notation to define shortcuts for the "X in t" part of a pattern.           *)
 Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope.
-Delimit Scope ssrpatternscope with pattern.
 
 (* Some shortcuts for recurrent "X in t" parts.                               *)
 Notation RHS := (X in _ = X)%pattern.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index bd9240476f..b67ac4f0df 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -10,6 +10,8 @@ Arguments Nat.sub !n !m.
 About Nat.sub.
 Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
   fun x => (f (fst x), g (snd x)).
+Declare Scope foo_scope.
+Declare Scope bar_scope.
 Delimit Scope foo_scope with F.
 Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
 About pf.
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39e..adab324cf0 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -76,6 +76,7 @@ Open Scope nat_scope.
 Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
 Coercion Zpos: nat >-> znat.
 
+Declare Scope znat_scope.
 Delimit Scope znat_scope with znat.
 Open Scope znat_scope.
 
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 66a82008d8..42af3583d4 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -757,6 +757,8 @@ Qed.
     with lazy behavior (for vm_compute)  *)
 (*****************************************)
 
+Declare Scope lazy_bool_scope.
+
 Notation "a &&& b" := (if a then b else false)
  (at level 40, left associativity) : lazy_bool_scope.
 Notation "a ||| b" := (if a then true else b)
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.
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 3485b9c68d..b0d1824827 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -25,6 +25,7 @@ Unset Strict Implicit.
 
 (** Notations and helper lemma about pairs *)
 
+Declare Scope pair_scope.
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 
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 :
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index b966f217aa..aec88f93bf 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -340,6 +340,8 @@ Functional Scheme union_ind := Induction for union Sort Prop.
 
 (** Notations and helper lemma about pairs and triples *)
 
+Declare Scope pair_scope.
+
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 3ba9d1f5ed..7b6740e94b 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -23,6 +23,7 @@ Inductive positive : Set :=
   | xO : positive -> positive
   | xH : positive.
 
+Declare Scope positive_scope.
 Delimit Scope positive_scope with positive.
 Bind Scope positive_scope with positive.
 Arguments xO _%positive.
@@ -37,6 +38,7 @@ Inductive N : Set :=
   | N0 : N
   | Npos : positive -> N.
 
+Declare Scope N_scope.
 Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Npos _%positive.
@@ -53,6 +55,7 @@ Inductive Z : Set :=
   | Zpos : positive -> Z
   | Zneg : positive -> Z.
 
+Declare Scope Z_scope.
 Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
 Arguments Zpos _%positive.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 39af62c32f..d91bfd4e2c 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -50,6 +50,7 @@ Inductive int31 : Type := I31 : digits31 int31.
 Register digits as int31 bits in "coq_int31" by True.
 Register int31 as int31 type in "coq_int31" by True.
 
+Declare Scope int31_scope.
 Delimit Scope int31_scope with int31.
 Bind Scope int31_scope with int31.
 Local Open Scope int31_scope.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d7f25a6613..ab17bb6e1a 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -46,6 +46,7 @@ Module ZEuclidProp
 
  (** We put notations in a scope, to avoid warnings about
      redefinitions of notations *)
+ Declare Scope euclid.
  Infix "/" := D.div : euclid.
  Infix "mod" := D.modulo : euclid.
  Local Open Scope euclid.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 4b2d5c13b5..995d96b314 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -13,15 +13,18 @@
 Require Import NSub ZAxioms.
 Require Export Ring.
 
+Declare Scope pair_scope.
+Local Open Scope pair_scope.
+
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-Local Open Scope pair_scope.
 
 Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
  Module Import NProp.
    Include NSubProp N.
  End NProp.
 
+Declare Scope NScope.
 Delimit Scope NScope with N.
 Bind Scope NScope with N.t.
 Infix "=="  := N.eq (at level 70) : NScope.
@@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
 
 End Z.
 
+Declare Scope ZScope.
 Delimit Scope ZScope with Z.
 Bind Scope ZScope with Z.t.
 Infix "=="  := Z.eq (at level 70) : ZScope.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 3d0c005fd1..acebfcf1d2 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -220,8 +220,10 @@ End NZDomainProp.
 Module NZOfNat (Import NZ:NZDomainSig').
 
 Definition ofnat (n : nat) : t := (S^n) 0.
-Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
+
+Declare Scope ofnat.
 Local Open Scope ofnat.
+Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
 
 Lemma ofnat_zero : [O] == 0.
 Proof.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index f55093ed48..c2316689fc 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) :=
 
 Hint Unfold compose.
 
+Declare Scope program_scope.
+
 Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : program_scope.
 
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 78c36dc7d1..c51cacac68 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -20,12 +20,13 @@ Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
+Declare Scope program_scope.
+Delimit Scope program_scope with prg.
+
 (** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _) : program_scope.
 
-Delimit Scope program_scope with prg.
-
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
 Notation " `  t " := (proj1_sig t) (at level 10, t at next level) : program_scope.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 35706e7fa2..139c4bf432 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -18,6 +18,7 @@ Require Export Morphisms Setoid Bool.
 
 Record Q : Set := Qmake {Qnum : Z; Qden : positive}.
 
+Declare Scope Q_scope.
 Delimit Scope Q_scope with Q.
 Bind Scope Q_scope with Q.
 Arguments Qmake _%Z _%positive.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 1510a7b825..81c318138e 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -18,6 +18,7 @@ Require Import Eqdep_dec.
 
 Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
 
+Declare Scope Qc_scope.
 Delimit Scope Qc_scope with Qc.
 Bind Scope Qc_scope with Qc.
 Arguments Qcmake this%Q _.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 36ac738ca6..9f8039ec9d 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -28,6 +28,7 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x.
 Definition comp f1 f2 (x:R) : R := f1 (f2 x).
 Definition inv_fct f (x:R) : R := / f x.
 
+Declare Scope Rfun_scope.
 Delimit Scope Rfun_scope with F.
 
 Arguments plus_fct (f1 f2)%F x%R.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 6019d4faf1..a2818371e9 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -14,6 +14,7 @@
 
 Require Export ZArith_base.
 Require Export Rdefinitions.
+Declare Scope R_scope.
 Local Open Scope R_scope.
 
 (*********************************************************)
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 87df6b479d..60c64d306b 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType').
   Module OrderTac := OT_to_OrderTac O.
   Ltac order := OrderTac.order.
 
+  Declare Scope order.
   Notation "x <= y" := (~lt y x) : order.
   Infix "?=" := compare (at level 70, no associativity) : order.
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index ba3e411091..390ca78c0e 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -305,6 +305,7 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni
 End VECTORLIST.
 
 Module VectorNotations.
+Declare Scope vector_scope.
 Delimit Scope vector_scope with vector.
 Notation "[ ]" := [] (format "[ ]") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 2f3bf9a32a..1e35370d29 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -17,6 +17,7 @@
 *)
 
 Require Import BinInt.
+Declare Scope Int_scope.
 Delimit Scope Int_scope with I.
 Local Open Scope Int_scope.
 
-- 
cgit v1.2.3


From 262a4e28744a81a433d387486d96a583f893c7e8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Mar 2018 14:03:07 +0200
Subject: CHANGES: mentioning new command "Declare Scope".

---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGES b/CHANGES
index 5d1c9a9c2d..738c0934d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,11 @@ Notations
 - New support for autonomous grammars of terms, called "custom
   entries" (see chapter "Syntax extensions" of the reference manual).
 
+- New command "Declare Scope" to explicitly declare a scope name
+  before any use of it. Implicit declaration of a scope at the time of
+  "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is
+  deprecated.
+
 Tactics
 
 - Added toplevel goal selector ! which expects a single focused goal.
-- 
cgit v1.2.3


From ace19eb0f555c6b2744bd23896e9459637d53394 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Jul 2018 10:28:32 +0200
Subject: Documenting "Declare Scope".

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index b46382dbbf..4c0e85bdd4 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and
 strings. However, this is only made possible at the Objective Caml
 level.
 
-See :ref:`above <NotationSyntax>` for the syntax of notations including the
-possibility to declare them in a given scope. Here is a typical example which
-declares the notation for conjunction in the scope ``type_scope``.
+.. cmd:: Declare Scope @scope
+
+   This adds a new scope named :n:`@scope`. Note that the initial
+   state of Coq declares by default the following interpretation scopes:
+   ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``,
+   ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``.
+
+The syntax to associate a notation to a scope is given
+:ref:`above <NotationSyntax>`. Here is a typical example which declares the
+notation for conjunction in the scope ``type_scope``.
 
 .. coqtop:: in
 
    Notation "A /\ B" := (and A B) : type_scope.
 
 .. note:: A notation not defined in a scope is called a *lonely*
-          notation.
+          notation. No example of lonely notations can be found in the
+          initial state of Coq though.
+
 
 Global interpretation rules for notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely
 interpretations and opening of scopes matters, and not the declaration
 of interpretations within a scope).
 
-The initial state of Coq declares three interpretation scopes and no
-lonely notations. These scopes, in opening order, are ``core_scope``,
-``type_scope`` and ``nat_scope``.
-
 .. cmd:: Open Scope @scope
 
    The command to add a scope to the interpretation scope stack is
-- 
cgit v1.2.3


From 0aa164f8fc8adf2cd57681ef64ff598c71b5d9f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Mar 2018 15:31:19 +0200
Subject: Declaring Scope prior to loading primitive printers.

---
 theories/Numbers/Cyclic/Int31/Int31.v | 3 +--
 theories/Reals/Rdefinitions.v         | 7 +++++--
 theories/Strings/Ascii.v              | 3 ++-
 theories/Strings/String.v             | 3 ++-
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d91bfd4e2c..77ab624ca5 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,8 +15,6 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
-Declare ML Module "int31_syntax_plugin".
-
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
@@ -51,6 +49,7 @@ Register digits as int31 bits in "coq_int31" by True.
 Register int31 as int31 type in "coq_int31" by True.
 
 Declare Scope int31_scope.
+Declare ML Module "int31_syntax_plugin".
 Delimit Scope int31_scope with int31.
 Bind Scope int31_scope with int31.
 Local Open Scope int31_scope.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 857b4ec33b..932fcddaf5 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -12,12 +12,15 @@
 (**          Definitions for the axiomatization          *)
 (*********************************************************)
 
-Declare ML Module "r_syntax_plugin".
 Require Export ZArith_base.
 
 Parameter R : Set.
 
-(* Declare Scope positive_scope with Key R *)
+(* Declare primitive numeral notations for Scope R_scope *)
+Declare Scope R_scope.
+Declare ML Module "r_syntax_plugin".
+
+(* Declare Scope R_scope with Key R *)
 Delimit Scope R_scope with R.
 
 (* Automatically open scope R_scope for arguments of type R *)
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 31a7fb8ad6..3f676c1888 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -13,7 +13,6 @@
     Adapted to Coq V8 by the Coq Development Team *)
 
 Require Import Bool BinPos BinNat PeanoNat Nnat.
-Declare ML Module "ascii_syntax_plugin".
 
 (** * Definition of ascii characters *)
 
@@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin".
 
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
+Declare Scope char_scope.
+Declare ML Module "ascii_syntax_plugin".
 Delimit Scope char_scope with char.
 Bind Scope char_scope with ascii.
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index be9a10c6dc..b27474ef25 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -15,7 +15,6 @@
 Require Import Arith.
 Require Import Ascii.
 Require Import Bool.
-Declare ML Module "string_syntax_plugin".
 
 (** *** Definition of strings *)
 
@@ -25,6 +24,8 @@ Inductive string : Set :=
   | EmptyString : string
   | String : ascii -> string -> string.
 
+Declare Scope string_scope.
+Declare ML Module "string_syntax_plugin".
 Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.
-- 
cgit v1.2.3