Protection des tactiques contre l'utilisation sans le bon contexte de thories

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

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