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

2 files changed, 41 insertions, 8 deletions

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