aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--library/library.ml16
1 files changed, 15 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index bc25eb617..93ab76371 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -471,7 +471,7 @@ let cache_require (_,(modl,export)) =
(* keeps the require marker for closed section replay but removes
OS dependent fields from .vo files for cross-platform compatibility *)
-let export_require (l,e) = Some (List.map (fun d -> d) l,e)
+let export_require (l,e) = Some (l,e)
let (in_require, out_require) =
declare_object
@@ -583,6 +583,20 @@ let fmt_modules_state () =
str "Loaded Modules: " ++
prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ())
+(*s For tactics/commands requiring vernacular libraries *)
+
+let check_required_module d =
+ let d' = List.map id_of_string d in
+ let dir = make_dirpath (List.rev d') in
+ if not (module_is_loaded dir) then
+(* Loading silently ...
+ let m, prefix = list_sep_last d' in
+ read_module
+ (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
+*)
+(* or failing ...*)
+ error ("Module "^(list_last d)^" has to be required first")
+
(*s Display the memory use of a module. *)
open Printf