Annotations at functor applications:

 - The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
 - The earlier syntax !F X should now be written "F X [no inline]"
   (note that using ! is still possible for compatibility)
 - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
   foo_scope by bar_scope in all arguments scope of objects in F.

 BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
 Arguments scope for lemmas are fixed for instances of Numbers.

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

19 files changed, 234 insertions, 193 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9403a4cca..476e2111e 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -90,6 +90,7 @@ Coercion
 Unification
 Cases
 Pretyping
+Declaremods
 
 Tok
 Lexer
diff --git a/interp/notation.ml b/interp/notation.ml
index 86a515537..6be016c18 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -435,7 +435,8 @@ open Classops
 
 let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
 
-let _ = Gmap.add CL_SORT "type_scope" Gmap.empty
+let _ =
+  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
 
 let declare_class_scope sc cl =
   class_scope_map := Gmap.add cl sc !class_scope_map
@@ -479,7 +480,9 @@ let cache_arguments_scope o =
   load_arguments_scope 1 o
 
 let subst_arguments_scope (subst,(req,r,scl)) =
-  (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
+  let r' = fst (subst_global subst r) in
+  let scl' = list_smartmap (Option.smartmap Declaremods.subst_scope) scl in
+  (ArgsScopeNoDischarge,r',scl')
 
 let discharge_arguments_scope (_,(req,r,l)) =
   if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
@@ -527,6 +530,7 @@ let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
   declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t)
 
+
 (********************************)
 (* Encoding notations as string *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 81b4e8e94..7539d8bd0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1218,17 +1218,6 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
-(* Which inline annotations should we honor, either None or the ones
-   whose level is less or equal to the given integer *)
-
-type inline = int option
-
-type module_ast_inl = module_ast * inline
-
-type 'a module_signature =
-  | Enforce of 'a (* ... : T *)
-  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
-
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
 (* and which are then occupied by proper symbols of the notation (or spaces) *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b7bac17bd..fad1281a6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -264,17 +264,6 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
-(* Which inline annotations should we honor, either None or the ones
-   whose level is less or equal to the given integer *)
-
-type inline = int option
-
-type module_ast_inl = module_ast * inline
-
-type 'a module_signature =
-  | Enforce of 'a (** ... : T *)
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-
 val ntn_loc :
   Util.loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b6b3a766f..68d928aef 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,8 +17,55 @@ open Lib
 open Nametab
 open Mod_subst
 
-(* modules and components *)
+(** Rigid / flexible signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+let scope_subst = ref (Stringmap.empty : string Stringmap.t)
+
+let add_scope_subst sc sc' =
+  scope_subst := Stringmap.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 Stringmap.find sc !scope_subst with Not_found -> sc
+
+let reset_scope_subst () =
+  scope_subst := Stringmap.empty
+
+(** Which inline annotations should we honor, either None or the ones
+    whose level is less or equal to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
+let default_inline () = Some (Flags.get_inline_level ())
 
+let inl2intopt = function
+  | NoInline -> None
+  | InlineAt i -> Some i
+  | DefaultInline -> default_inline ()
+
+type funct_app_annot =
+  { ann_inline : inline;
+    ann_scope_subst : scope_subst }
+
+let inline_annot a = inl2intopt a.ann_inline
+
+type 'a annotated = ('a * funct_app_annot)
+
+
+(* modules and components *)
 
 (* OBSOLETE This type is a functional closure of substitutive lib_objects.
 
@@ -78,7 +125,8 @@ let modtab_objects =
 let openmod_info =
   ref ((MPfile(initial_dir),[],None,[])
 	 : module_path *  mod_bound_id list *
-           (module_struct_entry * inline) option * module_type_body list)
+           (module_struct_entry * int option) option *
+	   module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -152,7 +200,8 @@ let funct_entry args m =
 
 let build_subtypes interp_modtype mp args mtys =
   List.map
-    (fun (m,inl) ->
+    (fun (m,ann) ->
+       let inl = inline_annot 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 =
@@ -465,18 +514,19 @@ let rec get_modtype_substobjs env mp_from inline = function
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
-  let process_arg id (mbid,(mty,inl)) =
+  let process_arg id (mbid,(mty,ann)) =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
     let (mbids,mp_from,objs) =
-      get_modtype_substobjs (Global.env()) mp inl mty in
+      get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in
     let substobjs = (mbids,mp,subst_objects
 		       (map_mp mp_from mp empty_delta_resolver) objs)in
       do_module false "start" load_objects 1 dir mp substobjs []
     in
       List.iter2 process_arg argids args
 
-let intern_args interp_modtype (idl,(arg,inl)) =
+let intern_args interp_modtype (idl,(arg,ann)) =
+  let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype (Global.env()) arg in
@@ -497,11 +547,12 @@ let start_module_ interp_modtype export id args res fs =
   let mp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
   let res_entry_o, sub_body_l = match res with
-    | Topconstr.Enforce (res,inl) ->
+    | Enforce (res,ann) ->
+        let inl = inline_annot 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), []
-    | Topconstr.Check resl ->
+    | Check resl ->
 	None, build_subtypes interp_modtype mp arg_entries resl
   in
   let mbids = List.map fst arg_entries in
@@ -691,7 +742,8 @@ let end_modtype () =
   mp
 
 
-let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
+let declare_modtype_ interp_modtype id args mtys (mty,ann) fs =
+  let inl = inline_annot 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
@@ -701,9 +753,11 @@ let declare_modtype_ interp_modtype id args mtys (mty,inl) 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 substobjs = (mbids,mmp,
 		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs)
   in
+  reset_scope_subst ();
   Summary.unfreeze_summaries fs;
   ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
@@ -744,17 +798,20 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
   let env = Global.env() in
-  let default_inl = Some (Flags.get_inline_level ()) in (* PLTODO *)
   let mty_entry_o, subs, inl_res = match res with
-    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
-    | Topconstr.Check mtys ->
-	None, build_subtypes interp_modtype mmp arg_entries mtys, default_inl
+    | Enforce (mty,ann) ->
+        Some (funct interp_modtype mty), [], inline_annot 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 = match mexpr_o with
-    | None -> None, default_inl
-    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
+  let mexpr_entry_o, inl_expr, scl = match mexpr_o with
+    | None -> None, default_inline (), []
+    | Some (mexpr,ann) ->
+      Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst
+
   in
   let entry =
     {mod_entry_type = mty_entry_o;
@@ -779,9 +836,10 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   
   check_subtypes mp subs;
-
+  register_scope_subst scl;
   let substobjs = (mbids,mp_env,
 		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  reset_scope_subst ();
   ignore (add_leaf
 	    id
 	    (in_module (Some (entry), substobjs)));
@@ -889,9 +947,13 @@ let get_includeself_substobjs env objs me is_mod inline =
     ([],mp_self,subst_objects subst objects)
   with NothingToDo -> objs
 
-let declare_one_include_inner inl (me,is_mod) =
+
+
+
+let declare_one_include_inner annot (me,is_mod) =
   let env = Global.env() in
   let mp1,_ = current_prefix () in
+  let inl = inline_annot annot in
   let (mbids,mp,objs)=
     if is_mod then
       get_module_substobjs env mp1 inl me
@@ -904,14 +966,16 @@ let declare_one_include_inner inl (me,is_mod) =
       (mbids,mp,objs) 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 substobjs = (mbids,mp1,
 		   subst_objects (map_mp mp mp1 resolver) objs) in
+  reset_scope_subst ();
   ignore (add_leaf id
 	    (in_include ((me,is_mod), substobjs)))
 
-let declare_one_include interp_struct me_ast =
-  declare_one_include_inner (snd me_ast)
-    (interp_struct (Global.env()) (fst me_ast))
+let declare_one_include interp_struct (me_ast,annot) =
+  declare_one_include_inner annot
+    (interp_struct (Global.env()) me_ast)
 
 let declare_include_ interp_struct me_asts =
   List.iter (declare_one_include interp_struct) me_asts
diff --git a/library/declaremods.mli b/library/declaremods.mli
index b1978c282..21a7aeabe 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -17,6 +17,33 @@ open Lib
 (** This modules provides official functions to declare modules and
   module types *)
 
+(** Rigid / flexible signature *)
+
+type 'a module_signature =
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+
+(** Should we adapt a few scopes during functor application ? *)
+
+type scope_subst = (string * string) list
+
+val subst_scope : string -> string
+
+(** Which inline annotations should we honor, either None or the ones
+   whose level is less or equal to the given integer *)
+
+type inline =
+  | NoInline
+  | DefaultInline
+  | InlineAt of int
+
+(** 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)
 
 (** {6 Modules } *)
 
@@ -37,13 +64,14 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
   identifier ->
-  (identifier located list * ('modast * inline)) list ->
-  ('modast * inline) Topconstr.module_signature ->
-  ('modast * inline) list -> module_path
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) module_signature ->
+  ('modast annotated) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
-  bool option -> identifier -> (identifier located list * ('modast * inline)) list ->
-  ('modast * inline) Topconstr.module_signature -> module_path
+  bool option -> identifier ->
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) module_signature -> module_path
 
 val end_module : unit -> module_path
 
@@ -53,12 +81,15 @@ val end_module : unit -> module_path
 
 val declare_modtype : (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
-  identifier -> (identifier located list * ('modast * inline)) list ->
-  ('modast * inline) list -> ('modast * inline) list -> module_path
+  identifier ->
+  (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) list ->
+  ('modast annotated) list ->
+  module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  identifier -> (identifier located list * ('modast * inline)) list ->
-  ('modast * inline) list -> module_path
+  identifier -> (identifier located list * ('modast annotated)) list ->
+  ('modast annotated) list -> module_path
 
 val end_modtype : unit -> module_path
 
@@ -103,7 +134,7 @@ val import_module : bool -> module_path -> unit
 (** Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
-  ('struct_expr * inline) list -> unit
+  ('struct_expr annotated) list -> unit
 
 (** {6 ... } *)
 (** [iter_all_segments] iterate over all segments, the modules'
@@ -120,5 +151,4 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 
 (** For translator *)
 val process_module_bindings : module_ident list ->
-  (mod_bound_id * (module_struct_entry * inline)) list -> unit
-
+  (mod_bound_id * (module_struct_entry annotated)) list -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0c7dbeeb0..e550cfa26 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -23,6 +23,7 @@ open Decl_kinds
 open Genarg
 open Ppextend
 open Goptions
+open Declaremods
 
 open Prim
 open Constr
@@ -444,15 +445,33 @@ GEXTEND Gram
     [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l)
       | -> [] ] ]
   ;
+  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 = [] }
+      ] ]
+  ;
   module_expr_inl:
-    [ [ "!"; me = module_expr -> (me,None)
-      | "<"; i = INT; ">"; me = module_expr -> (me,Some (int_of_string i))
-      | me = module_expr -> (me,Some (Flags.get_inline_level())) ] ]
+    [ [ "!"; me = module_expr ->
+        (me, { ann_inline = NoInline; ann_scope_subst = []})
+      | me = module_expr; a = functor_app_annots -> (me,a) ] ]
   ;
   module_type_inl:
-    [ [ "!"; me = module_type -> (me,None)
-      | "<"; i = INT; ">"; me = module_type -> (me,Some (int_of_string i))
-      | me = module_type -> (me,Some (Flags.get_inline_level())) ] ]
+    [ [ "!"; me = module_type ->
+        (me, { ann_inline = NoInline; ann_scope_subst = []})
+      | me = module_type; a = functor_app_annots -> (me,a) ] ]
   ;
   (* Module binder  *)
   module_binder:
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 42007e4b0..bba1e1a8f 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -24,6 +24,7 @@ open Ppextend
 open Topconstr
 open Decl_kinds
 open Tacinterp
+open Declaremods
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
@@ -227,8 +228,21 @@ 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_module_ast_inl pr_c (mast,o) =
-  (if o=None then str "!" else mt ()) ++ pr_module_ast pr_c mast
+let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
+  let sep () = if scl=[] then mt () else str "," in
+  if ann = DefaultInline && 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_of_module_type prc = function
   | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 583491386..9748a4366 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -24,65 +24,24 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 *)
 
+Delimit Scope bigZ_scope with bigZ.
 
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec
- <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+ ZMake.Make BigN [scope abstract_scope to bigZ_scope]
+ <+ ZTypeIsZAxioms [scope abstract_scope to bigZ_scope]
+ <+ ZProp [no inline, scope abstract_scope to bigZ_scope]
+ <+ HasEqBool2Dec [no inline, scope abstract_scope to bigZ_scope]
+ <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigZ_scope]
+ <+ MinMaxDecProperties [no inline, scope abstract_scope to bigZ_scope].
 
 (** Notations about [BigZ] *)
 
-Notation bigZ := BigZ.t.
+Local Open Scope bigZ_scope.
 
-Delimit Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with BigZ.t.
-Bind Scope bigZ_scope with BigZ.t_.
-(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
+Notation bigZ := BigZ.t.
+Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_.
 Arguments Scope BigZ.Pos [bigN_scope].
 Arguments Scope BigZ.Neg [bigN_scope].
-Arguments Scope BigZ.to_Z [bigZ_scope].
-Arguments Scope BigZ.succ [bigZ_scope].
-Arguments Scope BigZ.pred [bigZ_scope].
-Arguments Scope BigZ.opp [bigZ_scope].
-Arguments Scope BigZ.square [bigZ_scope].
-Arguments Scope BigZ.add [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.sub [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.mul [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.div [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.lt [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.le [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.compare [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.min [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.max [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope].
-Arguments Scope BigZ.pow_N [bigZ_scope N_scope].
-Arguments Scope BigZ.pow [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.log2 [bigZ_scope].
-Arguments Scope BigZ.sqrt [bigZ_scope].
-Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.rem [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.lcm [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.even [bigZ_scope].
-Arguments Scope BigZ.odd [bigZ_scope].
-Arguments Scope BigN.testbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.shiftl [bigZ_scope bigZ_scope].
-Arguments Scope BigN.shiftr [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lor [bigZ_scope bigZ_scope].
-Arguments Scope BigN.land [bigZ_scope bigZ_scope].
-Arguments Scope BigN.ldiff [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lxor [bigZ_scope bigZ_scope].
-Arguments Scope BigN.setbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.clearbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lnot [bigZ_scope].
-Arguments Scope BigN.div2 [bigZ_scope].
-Arguments Scope BigN.ones [bigZ_scope].
-
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
 Local Notation "2" := BigZ.two : bigZ_scope.
@@ -94,21 +53,19 @@ Infix "/" := BigZ.div : bigZ_scope.
 Infix "^" := BigZ.pow : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
-Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope.
+Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.
 Infix "<=" := BigZ.le : bigZ_scope.
-Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
-Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
-Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope.
-Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
-Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
-Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
+Notation "x > y" := (y < x) (only parsing) : bigZ_scope.
+Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope.
+Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope.
+Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope.
+Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
 Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
-Local Open Scope bigZ_scope.
-
 (** Some additional results about [BigZ] *)
 
 Theorem spec_to_Z: forall n : bigZ,
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 7534628fa..57b98e860 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -29,6 +29,8 @@ Module Make (N:NType) <: ZType.
 
  Definition t := t_.
 
+ Bind Scope abstract_scope with t t_.
+
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
  Definition two := Pos N.two.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 366418035..fbb91ef7f 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -223,8 +223,9 @@ Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZProp [scope abstract_scope to Z_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to Z_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to Z_scope].
 
 End Z.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 56fad9347..65b646356 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,6 +12,11 @@ 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 315876656..858c06658 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -26,62 +26,23 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 *)
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
- NMake.Make Int31Cyclic <+ NTypeIsNAxioms
- <+ !NProp <+ HasEqBool2Dec
- <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+Delimit Scope bigN_scope with bigN.
 
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+ NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]
+ <+ NTypeIsNAxioms [scope abstract_scope to bigN_scope]
+ <+ NProp [no inline, scope abstract_scope to bigN_scope]
+ <+ HasEqBool2Dec [no inline, scope abstract_scope to bigN_scope]
+ <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigN_scope]
+ <+ MinMaxDecProperties [no inline, scope abstract_scope to bigN_scope].
 
 (** Notations about [BigN] *)
 
-Notation bigN := BigN.t.
-
-Delimit Scope bigN_scope with bigN.
-Bind Scope bigN_scope with bigN.
-Bind Scope bigN_scope with BigN.t.
-Bind Scope bigN_scope with BigN.t'.
-(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
-Arguments Scope BigN.to_Z [bigN_scope].
-Arguments Scope BigN.to_N [bigN_scope].
-Arguments Scope BigN.succ [bigN_scope].
-Arguments Scope BigN.pred [bigN_scope].
-Arguments Scope BigN.square [bigN_scope].
-Arguments Scope BigN.add [bigN_scope bigN_scope].
-Arguments Scope BigN.sub [bigN_scope bigN_scope].
-Arguments Scope BigN.mul [bigN_scope bigN_scope].
-Arguments Scope BigN.div [bigN_scope bigN_scope].
-Arguments Scope BigN.eq [bigN_scope bigN_scope].
-Arguments Scope BigN.lt [bigN_scope bigN_scope].
-Arguments Scope BigN.le [bigN_scope bigN_scope].
-Arguments Scope BigN.eq [bigN_scope bigN_scope].
-Arguments Scope BigN.compare [bigN_scope bigN_scope].
-Arguments Scope BigN.min [bigN_scope bigN_scope].
-Arguments Scope BigN.max [bigN_scope bigN_scope].
-Arguments Scope BigN.eq_bool [bigN_scope bigN_scope].
-Arguments Scope BigN.pow_pos [bigN_scope positive_scope].
-Arguments Scope BigN.pow_N [bigN_scope N_scope].
-Arguments Scope BigN.pow [bigN_scope bigN_scope].
-Arguments Scope BigN.log2 [bigN_scope].
-Arguments Scope BigN.sqrt [bigN_scope].
-Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
-Arguments Scope BigN.modulo [bigN_scope bigN_scope].
-Arguments Scope BigN.gcd [bigN_scope bigN_scope].
-Arguments Scope BigN.lcm [bigN_scope bigN_scope].
-Arguments Scope BigN.even [bigN_scope].
-Arguments Scope BigN.odd [bigN_scope].
-Arguments Scope BigN.testbit [bigN_scope bigN_scope].
-Arguments Scope BigN.shiftl [bigN_scope bigN_scope].
-Arguments Scope BigN.shiftr [bigN_scope bigN_scope].
-Arguments Scope BigN.lor [bigN_scope bigN_scope].
-Arguments Scope BigN.land [bigN_scope bigN_scope].
-Arguments Scope BigN.ldiff [bigN_scope bigN_scope].
-Arguments Scope BigN.lxor [bigN_scope bigN_scope].
-Arguments Scope BigN.setbit [bigN_scope bigN_scope].
-Arguments Scope BigN.clearbit [bigN_scope bigN_scope].
-Arguments Scope BigN.lnot [bigN_scope bigN_scope].
-Arguments Scope BigN.div2 [bigN_scope].
-Arguments Scope BigN.ones [bigN_scope].
+Local Open Scope bigN_scope.
 
+Notation bigN := BigN.t.
+Bind Scope bigN_scope with bigN BigN.t BigN.t'.
+Arguments Scope BigN.N0 [int31_scope].
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
@@ -92,20 +53,18 @@ Infix "/" := BigN.div : bigN_scope.
 Infix "^" := BigN.pow : bigN_scope.
 Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
-Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope.
+Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
-Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
-Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
-Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope.
-Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope.
-Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope.
-Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope.
+Notation "x > y" := (y < x) (only parsing) : bigN_scope.
+Notation "x >= y" := (y <= x) (only parsing) : bigN_scope.
+Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
+Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
+Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
 
-Local Open Scope bigN_scope.
-
 (** Example of reasoning about [BigN] *)
 
 Theorem succ_pred: forall q : bigN,
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b5cc4c51d..f095a3482 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -138,6 +138,8 @@ 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/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index bd59ef494..cf284a2f1 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -234,8 +234,9 @@ Definition lor := Nor.
 Definition ldiff := Ndiff.
 Definition div2 := Ndiv2.
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp [scope abstract_scope to N_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope].
 
 End N.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0cf9ae441..4578851e2 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -756,8 +756,9 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
 
 (** Generic Properties *)
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp [scope abstract_scope to nat_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope].
 
 End Nat.
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2c90b6bd5..8ffdbdec4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -44,11 +44,11 @@ val interp_assumption :
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   Impargs.manual_implicits ->
-  bool (** implicit *) -> inline -> variable located -> unit
+  bool (** implicit *) -> Entries.inline -> variable located -> unit
 
 val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits ->
-  bool -> inline -> unit
+  bool -> Entries.inline -> unit
 
 (** {6 Inductive and coinductive types} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ccbaa6d30..ca4a82ea6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -32,6 +32,7 @@ open Pretyping
 open Redexpr
 open Syntax_def
 open Lemmas
+open Declaremods
 
 (* Pcoq hooks *)
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3091f10c5..ac3b3964a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -15,6 +15,7 @@ open Genarg
 open Topconstr
 open Decl_kinds
 open Ppextend
+open Declaremods
 
 (* Toplevel control exceptions *)
 exception Drop
@@ -168,6 +169,7 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
+type module_ast_inl = module_ast annotated
 type module_binder = bool option * lident list * module_ast_inl
 
 type grammar_tactic_prod_item_expr =