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

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 :