3 files changed, 6 insertions, 24 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 86a5155374..6be016c180 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 81b4e8e94d..7539d8bd0b 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 b7bac17bd0..fad1281a69 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 :