Add support for Local Declare ML Module

Instead of failing with some obscure error message *after* loading the
module, accept Local Declare ML Module with the usual semantics.

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

4 files changed, 19 insertions, 10 deletions

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 455e4286a6..367ae15675 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -230,7 +230,10 @@ let stdlib_use_plugins = Coq_config.has_natdynlink
  * (linked or loaded with load_object). It is used not to load a
  * module twice. It is NOT the list of ML modules Coq knows. *)
 
-type ml_module_object = { mnames : string list }
+type ml_module_object = {
+  mlocal : Vernacexpr.locality_flag;
+  mnames : string list
+}
 
 let known_loaded_modules = ref Stringset.empty
 
@@ -299,15 +302,18 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	      error ("Dynamic link not supported (module "^name^")")))
     mnames
 
+let classify_ml_module_object ({mlocal=mlocal} as o) =
+  if mlocal then Dispose else Substitute o
+
 let (inMLModule,outMLModule) =
   declare_object {(default_object "ML-MODULE") with
                     load_function = (fun _ -> cache_ml_module_object);
                     cache_function = cache_ml_module_object;
                     subst_function = (fun (_,_,o) -> o);
-                    classify_function = (fun o -> Substitute o) }
+                    classify_function = classify_ml_module_object }
 
-let declare_ml_modules l =
-  Lib.add_anonymous_leaf (inMLModule {mnames=l})
+let declare_ml_modules local l =
+  Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l})
 
 let print_ml_path () =
   let l = !coq_mlpath_copy in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 2b5de5708e..4230f0ee4b 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -59,11 +59,14 @@ val add_loaded_module : string -> unit
 val init_ml_modules : unit -> unit
 val unfreeze_ml_modules : string list -> unit
 
-type ml_module_object = { mnames: string list }
+type ml_module_object = {
+  mlocal: Vernacexpr.locality_flag;
+  mnames: string list;
+}
 val inMLModule : ml_module_object -> Libobject.obj
 val outMLModule : Libobject.obj -> ml_module_object
 
-val declare_ml_modules : string list -> unit
+val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
 val print_ml_path : unit -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5ee98db59f..e02079fad6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -706,8 +706,8 @@ let vernac_add_ml_path isrec path =
   (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
     (System.expand_path_macros path)
 
-let vernac_declare_ml_module l =
-  Mltop.declare_ml_modules (List.map System.expand_path_macros l)
+let vernac_declare_ml_module local l =
+  Mltop.declare_ml_modules local (List.map System.expand_path_macros l)
 
 let vernac_chdir = function
   | None -> message (Sys.getcwd())
@@ -1353,7 +1353,7 @@ let interp c = match c with
   | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
   | VernacRemoveLoadPath s -> vernac_remove_loadpath s
   | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s
-  | VernacDeclareMLModule l -> vernac_declare_ml_module l
+  | VernacDeclareMLModule (local, l) -> vernac_declare_ml_module local l
   | VernacChdir s -> vernac_chdir s
 
   (* State management *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 56fbd192bc..6a64fb1d5f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -276,7 +276,7 @@ type vernac_expr =
   | VernacAddLoadPath of rec_flag * lstring * dir_path option
   | VernacRemoveLoadPath of lstring
   | VernacAddMLPath of rec_flag * lstring
-  | VernacDeclareMLModule of lstring list
+  | VernacDeclareMLModule of locality_flag * lstring list
   | VernacChdir of lstring option
 
   (* State management *)