aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/ppvernac.ml3
-rw-r--r--plugins/interface/ascent.mli1
-rw-r--r--plugins/interface/vtp.ml3
-rw-r--r--plugins/interface/xlate.ml11
-rwxr-xr-xtools/coqdep_lexer.mll2
-rw-r--r--toplevel/mltop.ml414
-rw-r--r--toplevel/mltop.mli7
-rw-r--r--toplevel/vernacentries.ml6
-rw-r--r--toplevel/vernacexpr.ml2
10 files changed, 34 insertions, 17 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4cd798e3e..f66b4ed1e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,7 +582,7 @@ GEXTEND Gram
s = [ s = ne_string -> s | s = IDENT -> s ] ->
VernacLoad (verbosely, s)
| IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
- VernacDeclareMLModule l
+ VernacDeclareMLModule (use_locality (), l)
| IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
error "This command is deprecated, use Print Universes"
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 95e921a24..9f185c260 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -800,7 +800,8 @@ let rec pr_vernac = function
| VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
| VernacAddMLPath (fl,s) ->
str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
- | VernacDeclareMLModule l ->
+ | VernacDeclareMLModule (local, l) ->
+ pr_locality local ++
hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
| VernacChdir s -> str"Cd" ++ pr_opt qs s
diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli
index f0b68fb7c..bc615f14e 100644
--- a/plugins/interface/ascent.mli
+++ b/plugins/interface/ascent.mli
@@ -107,6 +107,7 @@ and ct_COMMAND =
| CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST
| CT_ml_add_path of ct_STRING
| CT_ml_declare_modules of ct_STRING_NE_LIST
+ | CT_local_ml_declare_modules of ct_STRING_NE_LIST
| CT_ml_print_modules
| CT_ml_print_path
| CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
diff --git a/plugins/interface/vtp.ml b/plugins/interface/vtp.ml
index 1714440df..a84f9ea56 100644
--- a/plugins/interface/vtp.ml
+++ b/plugins/interface/vtp.ml
@@ -373,6 +373,9 @@ and fCOMMAND = function
| CT_ml_declare_modules(x1) ->
fSTRING_NE_LIST x1 ++
fNODE "ml_declare_modules" 1
+| CT_local_ml_declare_modules(x1) ->
+ fSTRING_NE_LIST x1 ++
+ fNODE "local_ml_declare_modules" 1
| CT_ml_print_modules -> fNODE "ml_print_modules" 0
| CT_ml_print_path -> fNODE "ml_print_path" 0
| CT_module(x1, x2, x3, x4) ->
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 613c31db7..d294af68d 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1671,10 +1671,13 @@ let rec xlate_vernac =
(*ML commands *)
| VernacAddMLPath (false,str) -> CT_ml_add_path (CT_string str)
| VernacAddMLPath (true,str) -> CT_rec_ml_add_path (CT_string str)
- | VernacDeclareMLModule [] -> failwith ""
- | VernacDeclareMLModule (str :: l) ->
- CT_ml_declare_modules
- (CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l))
+ | VernacDeclareMLModule (_, []) -> failwith ""
+ | VernacDeclareMLModule (local, (str :: l)) ->
+ let x = CT_string_ne_list (CT_string str, List.map (fun x -> CT_string x) l) in
+ if local then
+ CT_local_ml_declare_modules x
+ else
+ CT_ml_declare_modules x
| VernacGoal c ->
CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_formula c))
| VernacAbort (Some (_,id)) ->
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index b13c16bad..89eeed54a 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -55,7 +55,7 @@ rule coq_action = parse
{ module_names := []; opened_file lexbuf}
| "Require" space+ "Import" space+
{ module_names := []; opened_file lexbuf}
- | "Declare" space+ "ML" space+ "Module" space+
+ | "Local"? "Declare" space+ "ML" space+ "Module" space+
{ mllist := []; modules lexbuf}
| "Load" space+
{ load_file lexbuf }
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 455e4286a..367ae1567 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 2b5de5708..4230f0ee4 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 5ee98db59..e02079fad 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 56fbd192b..6a64fb1d5 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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-15 10:44:52 +0000