Variant !F M for functor application that does not honor the Inline declarations

 For F(X:T), the application !F M works as F M, except that if module type T
 contains some "Inline" annotations, they are not taken in account when substituting
 X with M in F. See forthcoming commits for examples of use for this feature.

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

2 files changed, 29 insertions, 20 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f4d588b572..f0d90b11b8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -380,7 +380,7 @@ GEXTEND Gram
 	body = is_module_type ->
 	  VernacDeclareModuleType (id, bl, sign, body)
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
-	bl = LIST0 module_binder; ":"; mty = module_type ->
+	bl = LIST0 module_binder; ":"; mty = module_type_inl ->
 	  VernacDeclareModule (export, id, bl, mty)
       (* Section beginning *)
       | IDENT "Section"; id = identref -> VernacBeginSection id
@@ -396,9 +396,9 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr ->
+      | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
-      | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type ->
+      | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  warning "Include Type is deprecated; use Include instead";
           VernacInclude(e::l) ] ]
   ;
@@ -408,36 +408,42 @@ GEXTEND Gram
       |  -> None ] ]
   ;
   ext_module_type:
-    [ [ "<+"; mty = module_type -> mty ] ]
+    [ [ "<+"; mty = module_type_inl -> mty ] ]
   ;
   ext_module_expr:
-    [ [ "<+"; mexpr = module_expr -> mexpr ] ]
+    [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ]
   ;
   check_module_type:
-    [ [ "<:"; mty = module_type -> mty ] ]
+    [ [ "<:"; mty = module_type_inl -> mty ] ]
   ;
   check_module_types:
     [ [ mtys = LIST0 check_module_type -> mtys ] ]
   ;
   of_module_type:
-    [ [ ":"; mty = module_type -> Enforce mty
+    [ [ ":"; mty = module_type_inl -> Enforce mty
       | mtys = check_module_types -> Check mtys ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l)
+    [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l)
       | -> [] ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l)
+    [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l)
       | -> [] ] ]
   ;
-
+  module_expr_inl:
+    [ [ "!"; me = module_expr -> (me,false)
+      | me = module_expr -> (me,true) ] ]
+  ;
+  module_type_inl:
+    [ [ "!"; me = module_type -> (me,false)
+      | me = module_type -> (me,true) ] ]
+  ;
   (* Module binder  *)
   module_binder:
     [ [ "("; export = export_token; idl = LIST1 identref; ":";
-         mty = module_type; ")" -> (export,idl,mty) ] ]
+         mty = module_type_inl; ")" -> (export,idl,mty) ] ]
   ;
-
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 92a455abce..6d3cf76b27 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -246,24 +246,27 @@ 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,b) =
+  (if b then mt () else str "!") ++ pr_module_ast pr_c mast
+
 let pr_of_module_type prc = function
-  | Enforce mty -> str ":" ++ pr_module_ast prc mty
+  | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
   | Check mtys ->
-      prlist_strict (fun m -> str "<:" ++ pr_module_ast prc m) mtys
+      prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl prc m) mtys
 
 let pr_require_token = function
   | Some true -> str "Export "
   | Some false -> str "Import "
   | None -> mt()
 
-let pr_module_vardecls pr_c (export,idl,mty) =
+let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
   let m = pr_module_ast pr_c mty in
   (* Update the Nametab for interpreting the body of module/modtype *)
   let lib_dir = Lib.library_dp() in
   List.iter (fun (_,id) ->
     Declaremods.process_module_bindings [id]
       [make_mbid lib_dir (string_of_id id),
-       Modintern.interp_modtype (Global.env()) mty]) idl;
+       (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
   (* Builds the stream *)
   spc() ++
   hov 1 (str"(" ++ pr_require_token export ++
@@ -745,21 +748,21 @@ let rec pr_vernac = function
                pr_of_module_type pr_lconstr tys ++
 	       (if bd = [] then mt () else str ":= ") ++
 	       prlist_with_sep (fun () -> str " <+ ")
-	        (pr_module_ast pr_lconstr) bd)
+	        (pr_module_ast_inl pr_lconstr) bd)
   | VernacDeclareModule (export,id,bl,m1) ->
       let b = pr_module_binders_list bl pr_lconstr in
 	hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++
              pr_lident id ++ b ++
-             pr_module_ast pr_lconstr m1)
+             pr_module_ast_inl pr_lconstr m1)
   | VernacDeclareModuleType (id,bl,tyl,m) ->
       let b = pr_module_binders_list bl pr_lconstr in
-      let pr_mt = pr_module_ast pr_lconstr in
+      let pr_mt = pr_module_ast_inl pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
 		 prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
 		 (if m = [] then mt () else str ":= ") ++
 		 prlist_with_sep (fun () -> str " <+ ") pr_mt m)
   | VernacInclude (mexprs) ->
-      let pr_m = pr_module_ast pr_lconstr in
+      let pr_m = pr_module_ast_inl pr_lconstr in
       hov 2 (str"Include " ++
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)