More dynamic argument scopes

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 163 insertions, 162 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 8ec578621..a5a6138f6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -546,10 +546,10 @@ end
 
 module ScopeClassMap = Map.Make(ScopeClassOrd)
 
-let scope_class_map = ref (ScopeClassMap.empty : scope_name ScopeClassMap.t)
+let initial_scope_class_map : scope_name ScopeClassMap.t =
+  ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
 
-let _ =
-  scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+let scope_class_map = ref initial_scope_class_map
 
 let declare_scope_class sc cl =
   scope_class_map := ScopeClassMap.add cl sc !scope_class_map
@@ -584,15 +584,20 @@ let compute_type_scope t =
 let compute_scope_of_global ref =
   find_scope_class_opt (Some (ScopeRef ref))
 
-(** When merging scope list, we give priority to the first one (computed
-    by substitution), using the second one (user given or earlier automatic)
-    as fallback *)
+(** Updating a scope list, thanks to a list of argument classes
+    and the current Bind Scope base. When some current scope
+    have been manually given, the corresponding argument class
+    is emptied below, so this manual scope will be preserved. *)
+
+let update_scope cl sco =
+  match find_scope_class_opt cl with
+  | None -> sco
+  | sco' -> sco'
 
-let rec merge_scope sc1 sc2 = match sc1, sc2 with
-  | [], _ -> sc2
-  | _, [] -> sc1
-  | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
-  | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+let rec update_scopes cls scl = match cls, scl with
+  | [], _ -> scl
+  | _, [] -> List.map find_scope_class_opt cls
+  | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl
 
 let arguments_scope = ref Refmap.empty
 
@@ -603,7 +608,8 @@ type arguments_scope_discharge_request =
 
 let load_arguments_scope _ (_,(_,r,scl,cls)) =
   List.iter (Option.iter check_scope) scl;
-  arguments_scope := Refmap.add r (scl,cls) !arguments_scope
+  let initial_stamp = ScopeClassMap.empty in
+  arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
@@ -624,9 +630,7 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
   let cls' = List.smartmap subst_cl cls in
-  let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
-  let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
-  (ArgsScopeNoDischarge,r',scl'',cls')
+  (ArgsScopeNoDischarge,r',scl,cls')
 
 let discharge_arguments_scope (_,(req,r,l,_)) =
   if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
@@ -643,10 +647,13 @@ let rebuild_arguments_scope (req,r,l,_) =
 	(req,r,scs,cls)
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
-           for the extra parameters of the section *)
+           for the extra parameters of the section. Discard the classes
+           of the manually given scopes to avoid further re-computations. *)
 	let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
-	let l1,_ = List.chop (List.length l' - List.length l) l' in
-	(req,r,l1@l,cls)
+        let nparams = List.length l' - List.length l in
+	let l1 = List.firstn nparams l' in
+        let cls1 = List.firstn nparams cls in
+	(req,r,l1@l,cls1)
 
 type arguments_scope_obj =
     arguments_scope_discharge_request * global_reference *
@@ -666,13 +673,23 @@ let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 let declare_arguments_scope_gen req r (scl,cls) =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
 
-let declare_arguments_scope local ref scl =
-  let req =
-    if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
-  declare_arguments_scope_gen req ref (scl,[])
+let declare_arguments_scope local r scl =
+  let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
+  in
+  (* We empty the list of argument classes to disable futher scope
+     re-computations and keep these manually given scopes. *)
+  declare_arguments_scope_gen req r (scl,[])
 
 let find_arguments_scope r =
-  try fst (Refmap.find r !arguments_scope)
+  try
+    let (scl,cls,stamp) = Refmap.find r !arguments_scope in
+    let cur_stamp = !scope_class_map in
+    if stamp == cur_stamp then scl
+    else
+      (* Recent changes in the Bind Scope base, we re-compute the scopes *)
+      let scl' = update_scopes cls scl in
+      arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope;
+      scl'
   with Not_found -> []
 
 let declare_ref_arguments_scope ref =
@@ -959,7 +976,7 @@ let init () =
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
   printing_rules := String.Map.empty;
-  scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+  scope_class_map := initial_scope_class_map
 
 let _ =
   Summary.declare_summary "symbols"
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f0f565b53..a780ac0f1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -230,19 +230,7 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
-(** Should we adapt a few scopes during functor application ? *)
-
-type scope_subst = (string * string) list
-
-(** The type of annotations for functor applications *)
-
-type funct_app_annot =
-  { ann_inline : inline;
-    ann_scope_subst : scope_subst }
-
-type 'a annotated = ('a * funct_app_annot)
-
-type module_ast_inl = module_ast annotated
+type module_ast_inl = module_ast * inline
 type module_binder = bool option * lident list * module_ast_inl
 
 (** {6 The type of vernacular expressions} *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 15a964792..a5804eb53 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -18,19 +18,7 @@ open Lib
 open Mod_subst
 open Vernacexpr
 
-let scope_subst = ref (String.Map.empty : string String.Map.t)
-
-let add_scope_subst sc sc' =
-  scope_subst := String.Map.add sc sc' !scope_subst
-
-let register_scope_subst scl =
-  List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl
-
-let subst_scope sc =
- try String.Map.find sc !scope_subst with Not_found -> sc
-
-let reset_scope_subst () =
-  scope_subst := String.Map.empty
+(** {6 Inlining levels} *)
 
 let default_inline () = Some (Flags.get_inline_level ())
 
@@ -39,8 +27,6 @@ let inl2intopt = function
   | InlineAt i -> Some i
   | DefaultInline -> default_inline ()
 
-let inline_annot a = inl2intopt a.ann_inline
-
 (* modules and components *)
 
 (* This type is for substitutive lib_objects.
@@ -168,7 +154,7 @@ let funct_entry args m =
 let build_subtypes interp_modtype mp args mtys =
   List.map
     (fun (m,ann) ->
-       let inl = inline_annot ann in
+       let inl = inl2intopt ann in
        let mte = interp_modtype (Global.env()) m in
        let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
        let funct_mtb =
@@ -462,7 +448,7 @@ let process_module_seb_binding mbid seb =
   process_module_binding mbid (seb2mse seb)
 
 let intern_args interp_modtype (idl,(arg,ann)) =
-  let inl = inline_annot ann in
+  let inl = inl2intopt ann in
   let lib_dir = Lib.library_dp() in
   let env = Global.env() in
   let mty = interp_modtype env arg in
@@ -484,7 +470,7 @@ let start_module_ interp_modtype export id args res fs =
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
   let res_entry_o, subtyps = match res with
     | Enforce (res,ann) ->
-        let inl = inline_annot ann in
+        let inl = inl2intopt ann in
 	let mte = interp_modtype (Global.env()) res in
 	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
 	Some (mte,inl), []
@@ -675,7 +661,7 @@ let end_modtype () =
 
 
 let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
-  let inl = inline_annot ann in
+  let inl = inl2intopt ann in
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
   let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
@@ -685,10 +671,8 @@ let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
   (* Undo the simulated interactive building of the module type *)
   (* and declare the module type as a whole *)
 
-  register_scope_subst ann.ann_scope_subst;
   let subst = map_mp mp_from mmp empty_delta_resolver in
   let substobjs = (mbids,mmp, subst_objects subst objs) in
-  reset_scope_subst ();
   Summary.unfreeze_summaries fs;
   ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
@@ -731,17 +715,17 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   let env = Global.env() in
   let mty_entry_o, subs, inl_res = match res with
     | Enforce (mty,ann) ->
-        Some (funct interp_modtype mty), [], inline_annot ann
+        Some (funct interp_modtype mty), [], inl2intopt ann
     | Check mtys ->
 	None, build_subtypes interp_modtype mmp arg_entries mtys,
         default_inline ()
   in
  
   (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
-  let mexpr_entry_o, inl_expr, scl = match mexpr_o with
-    | None -> None, default_inline (), []
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, default_inline ()
     | Some (mexpr,ann) ->
-      Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst
+      Some (funct interp_modexpr mexpr), inl2intopt ann
 
   in
   let entry =
@@ -770,10 +754,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   then anomaly (Pp.str "Kernel and Library names do not match");
 
   check_subtypes mp subs;
-  register_scope_subst scl;
   let subst = map_mp mp_from mp_env resolver in
   let substobjs = (mbids,mp_env, subst_objects subst objs) in
-  reset_scope_subst ();
   ignore (add_leaf id (in_module substobjs));
   mmp
 
@@ -853,7 +835,7 @@ let get_includeself_substobjs env mp1 mbids objs me is_mod inline =
 let declare_one_include_inner annot (me,is_mod) =
   let env = Global.env() in
   let cur_mp = fst (current_prefix ()) in
-  let inl = inline_annot annot in
+  let inl = inl2intopt annot in
   let (mbids,mp,objs)=
     if is_mod then
       get_module_substobjs env inl me
@@ -865,10 +847,8 @@ let declare_one_include_inner annot (me,is_mod) =
   in
   let id = current_mod_id() in
   let resolver = Global.add_include me is_mod inl in
-  register_scope_subst annot.ann_scope_subst;
   let subst = map_mp mp cur_mp resolver in
   let substobjs = subst_objects subst objs in
-  reset_scope_subst ();
   ignore (add_leaf id (in_include substobjs))
 
 let declare_one_include interp_struct (me_ast,annot) =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 06a4edd84..b76017286 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -16,11 +16,6 @@ open Libobject
 open Lib
 open Vernacexpr
 
-(** This modules provides official functions to declare modules and
-  module types *)
-
-val subst_scope : string -> string
-
 (** {6 Modules } *)
 
 (** [declare_module interp_modtype interp_modexpr id fargs typ expr]
@@ -40,14 +35,14 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   Id.t ->
-  (Id.t located list * ('modast annotated)) list ->
-  ('modast annotated) module_signature ->
-  ('modast annotated) list -> module_path
+  (Id.t located list * ('modast * inline)) list ->
+  ('modast * inline) module_signature ->
+  ('modast * inline) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
   bool option -> Id.t ->
-  (Id.t located list * ('modast annotated)) list ->
-  ('modast annotated) module_signature -> module_path
+  (Id.t located list * ('modast * inline)) list ->
+  ('modast * inline) module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -58,14 +53,14 @@ val end_module : unit -> module_path
 val declare_modtype : (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   Id.t ->
-  (Id.t located list * ('modast annotated)) list ->
-  ('modast annotated) list ->
-  ('modast annotated) list ->
+  (Id.t located list * ('modast * inline)) list ->
+  ('modast * inline) list ->
+  ('modast * inline) list ->
   module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  Id.t -> (Id.t located list * ('modast annotated)) list ->
-  ('modast annotated) list -> module_path
+  Id.t -> (Id.t located list * ('modast * inline)) list ->
+  ('modast * inline) list -> module_path
 
 val end_modtype : unit -> module_path
 
@@ -110,7 +105,7 @@ val import_module : bool -> module_path -> unit
 (** Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
-  ('struct_expr annotated) list -> unit
+  ('struct_expr * inline) list -> unit
 
 (** {6 ... } *)
 (** [iter_all_segments] iterate over all segments, the modules'
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bc07fe896..450414625 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -455,32 +455,19 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   functor_app_annot:
-    [ [ IDENT "inline"; "at"; IDENT "level"; i = INT ->
-        [InlineAt (int_of_string i)], []
-      | IDENT "no"; IDENT "inline" -> [NoInline], []
-      | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2]
-      ] ]
-  ;
-  functor_app_annots:
-    [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" ->
-        let inl,scs = List.split l in
-	let inl = match List.concat inl with
-	  | [] -> DefaultInline
-	  | [inl] -> inl
-	  | _ -> error "Functor application with redundant inline annotations"
-	in { ann_inline = inl; ann_scope_subst = List.concat scs }
-      | -> { ann_inline = DefaultInline; ann_scope_subst = [] }
+    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" ->
+        InlineAt (int_of_string i)
+      | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline
+      | -> DefaultInline
       ] ]
   ;
   module_expr_inl:
-    [ [ "!"; me = module_expr ->
-        (me, { ann_inline = NoInline; ann_scope_subst = []})
-      | me = module_expr; a = functor_app_annots -> (me,a) ] ]
+    [ [ "!"; me = module_expr -> (me,NoInline)
+      | me = module_expr; a = functor_app_annot -> (me,a) ] ]
   ;
   module_type_inl:
-    [ [ "!"; me = module_type ->
-        (me, { ann_inline = NoInline; ann_scope_subst = []})
-      | me = module_type; a = functor_app_annots -> (me,a) ] ]
+    [ [ "!"; me = module_type -> (me,NoInline)
+      | me = module_type; a = functor_app_annot -> (me,a) ] ]
   ;
   (* Module binder  *)
   module_binder:
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d8ddb275d..3c4f25880 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -222,21 +222,13 @@ let rec pr_module_ast pr_c = function
       pr_module_ast pr_c me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
 
-let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
-  let sep () = if List.is_empty scl then mt () else str "," in
-  if ann == DefaultInline && List.is_empty scl then mt ()
-  else
-    str " [" ++
-    (match ann with
-      | DefaultInline -> mt ()
-      | NoInline -> str "no inline" ++ sep ()
-      | InlineAt i -> str "inline at level " ++ int i ++ sep ()) ++
-    prlist_with_sep (fun () -> str ", ")
-      (fun (sc1,sc2) -> str ("scope "^sc1^" to "^sc2)) scl ++
-    str "]"
-
-let pr_module_ast_inl pr_c (mast,ann) =
-  pr_module_ast pr_c mast ++ pr_annot ann
+let pr_inline = function
+  | DefaultInline -> mt ()
+  | NoInline -> str "[no inline]"
+  | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+let pr_module_ast_inl pr_c (mast,inl) =
+  pr_module_ast pr_c mast ++ pr_inline inl
 
 let pr_of_module_type prc = function
   | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v
new file mode 100644
index 000000000..ca9457be7
--- /dev/null
+++ b/test-suite/success/NumberScopes.v
@@ -0,0 +1,62 @@
+
+(* We check that various definitions or lemmas have the correct
+   argument scopes, especially the ones created via functor application. *)
+
+Close Scope nat_scope.
+
+Require Import PArith.
+Check (Pos.add 1 2).
+Check (Pos.add_comm 1 2).
+Check (Pos.min_comm 1 2).
+Definition f_pos (x:positive) := x.
+Definition f_pos' (x:Pos.t) := x.
+Check (f_pos 1).
+Check (f_pos' 1).
+
+Require Import ZArith.
+Check (Z.add 1 2).
+Check (Z.add_comm 1 2).
+Check (Z.min_comm 1 2).
+Definition f_Z (x:Z) := x.
+Definition f_Z' (x:Z.t) := x.
+Check (f_Z 1).
+Check (f_Z' 1).
+
+Require Import NArith.
+Check (N.add 1 2).
+Check (N.add_comm 1 2).
+Check (N.min_comm 1 2).
+Definition f_N (x:N) := x.
+Definition f_N' (x:N.t) := x.
+Check (f_N 1).
+Check (f_N' 1).
+
+Require Import NPeano.
+Check (Nat.add 1 2).
+Check (Nat.add_comm 1 2).
+Check (Nat.min_comm 1 2).
+Definition f_nat (x:nat) := x.
+Definition f_nat' (x:Nat.t) := x.
+Check (f_nat 1).
+Check (f_nat' 1).
+
+Require Import BigN.
+Check (BigN.add 1 2).
+Check (BigN.add_comm 1 2).
+Check (BigN.min_comm 1 2).
+Definition f_bigN (x:bigN) := x.
+Check (f_bigN 1).
+
+Require Import BigZ.
+Check (BigZ.add 1 2).
+Check (BigZ.add_comm 1 2).
+Check (BigZ.min_comm 1 2).
+Definition f_bigZ (x:bigZ) := x.
+Check (f_bigZ 1).
+
+Require Import BigQ.
+Check (BigQ.add 1 2).
+Check (BigQ.add_comm 1 2).
+Check (BigQ.min_comm 1 2).
+Definition f_bigQ (x:bigQ) := x.
+Check (f_bigQ 1).
\ No newline at end of file
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5b1e83e6c..61a77bf0e 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -893,11 +893,9 @@ Qed.
 
 (** Instantiation of generic properties of natural numbers *)
 
-(** The Bind Scope prevents N to stay associated with abstract_scope.
-    (TODO FIX) *)
-
-Include NProp. Bind Scope N_scope with N.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -983,6 +981,8 @@ Qed.
 
 End N.
 
+Bind Scope N_scope with N.t N.
+
 (** Exportation of notations *)
 
 Infix "+" := N.add : N_scope.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index a56f90b08..eca97ace9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -26,15 +26,13 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Delimit Scope bigZ_scope with bigZ.
 
-Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
- Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
- Bind Scope bigZ_scope with t t_.
- Include ZTypeIsZAxioms
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
+ ZMake.Make BigN
+ <+ ZTypeIsZAxioms
  <+ ZProp [no inline]
  <+ HasEqBool2Dec [no inline]
  <+ MinMaxLogicalProperties [no inline]
  <+ MinMaxDecProperties [no inline].
-End BigZ.
 
 (** For precision concerning the above scope handling, see comment in BigN *)
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 180fe0a96..28c298dbe 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -29,8 +29,6 @@ Module Make (NN:NType) <: ZType.
 
  Definition t := t_.
 
- Bind Scope abstract_scope with t t_.
-
  Definition zero := Pos NN.zero.
  Definition one  := Pos NN.one.
  Definition two := Pos NN.two.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 62b148294..f073cae89 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,11 +12,6 @@ Require Import NZAxioms.
 
 Module Type NZBaseProp (Import NZ : NZDomainSig').
 
-(** An artificial scope meant to be substituted later *)
-
-Delimit Scope abstract_scope with abstract.
-Bind Scope abstract_scope with t.
-
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
 Lemma eq_sym_iff : forall x y, x==y <-> y==x.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 072b75f78..380963cff 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 Delimit Scope bigN_scope with bigN.
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
- Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
- Bind Scope bigN_scope with t t'.
- Include NTypeIsNAxioms
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+  NMake.Make Int31Cyclic
+  <+ NTypeIsNAxioms
   <+ NProp [no inline]
   <+ HasEqBool2Dec [no inline]
   <+ MinMaxLogicalProperties [no inline]
   <+ MinMaxDecProperties [no inline].
-End BigN.
-
-(** Nota concerning scopes : for the first Include, we cannot bind
-    the scope bigN_scope to a type that doesn't exists yet.
-    We hence need to explicitely declare the scope substitution.
-    For the next Include, the abstract type t (in scope abstract_scope)
-    gets substituted to concrete BigN.t (in scope bigN_scope),
-    and the corresponding argument scope are fixed automatically.
-*)
 
 (** Notations about [BigN] *)
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b941ed48f..b28ce15b9 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -138,8 +138,6 @@ pr
   pr "";
   pr " Definition t := t'.";
   pr "";
-  pr " Bind Scope abstract_scope with t t'.";
-  pr "";
 
   pr " (** * A generic toolbox for building and deconstructing [t] *)";
   pr "";
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index a510b3ae2..5e36916b9 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -800,6 +800,8 @@ Include NProp
 
 End Nat.
 
+Bind Scope nat_scope with Nat.t nat.
+
 (** [Nat] contains an [order] tactic for natural numbers *)
 
 (** Note that [Nat.order] is domain-agnostic: it will not prove
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index a2bc5e266..50c90757a 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -38,9 +38,8 @@ End BigN_BigZ.
 Delimit Scope bigQ_scope with bigQ.
 
 Module BigQ <: QType <: OrderedTypeFull <: TotalOrder.
- Include QMake.Make BigN BigZ BigN_BigZ [scope abstract_scope to bigQ_scope].
- Bind Scope bigQ_scope with t t_.
- Include !QProperties <+ HasEqBool2Dec
+ Include QMake.Make BigN BigZ BigN_BigZ
+  <+ !QProperties <+ HasEqBool2Dec
   <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
  Ltac order := Private_Tac.order.
 End BigQ.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index a13bb5114..167be6d70 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -39,8 +39,6 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  Definition t := t_.
 
- Bind Scope abstract_scope with t t_.
-
  (** Specification with respect to [QArith] *)
 
  Local Open Scope Q_scope.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index be5858718..aa065e3c5 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1840,6 +1840,8 @@ Qed.
 
 End Pos.
 
+Bind Scope positive_scope with Pos.t positive.
+
 (** Exportation of notations *)
 
 Infix "+" := Pos.add : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index eeec9042f..6948d420a 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1153,11 +1153,9 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
 Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
 Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
-(** The Bind Scope prevents Z to stay associated with abstract_scope.
-    (TODO FIX) *)
-
-Include ZProp. Bind Scope Z_scope with Z.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1277,6 +1275,8 @@ Qed.
 
 End Z.
 
+Bind Scope Z_scope with Z.t Z.
+
 (** Re-export Notations *)
 
 Infix "+" := Z.add : Z_scope.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0c95201d2..8ec699c71 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1280,7 +1280,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with
   | ScopeClasses cl ->
       let cl' = List.map_filter (subst_scope_class subst) cl in
       let cl' =
-        if Int.equal (List.length cl) (List.length cl') && List.for_all2 (==) cl cl' then cl
+        if List.for_all2eq (==) cl cl' then cl
         else cl' in
       scope, ScopeClasses cl'
   | _ -> x