Nettoyage et documentation de Library

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

2 files changed, 24 insertions, 0 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 113cb9d3f..fa939d0aa 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -16,6 +16,9 @@ open Libnames
 open Pattern
 open Nametab
 
+(************************************************************************)
+(* Generic functions to find Coq objects *)
+
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let gen_reference locstr dir s =
@@ -58,6 +61,24 @@ let gen_constant_in_modules locstr dirs s =
 	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
 	prlist_with_sep pr_coma pr_dirpath dirs)
 
+
+(* For tactics/commands requiring vernacular libraries *)
+
+let check_required_library d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_loaded dir) then
+(* Loading silently ...
+    let m, prefix = list_sep_last d' in
+    read_library 
+     (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
+*)
+(* or failing ...*)
+    error ("Library "^(list_last d)^" has to be required first")
+
+(************************************************************************)
+(* Specific Coq objects *)
+
 let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
 
 let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s  
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 6741e1a0a..64c83d7eb 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -31,6 +31,9 @@ val arith_modules : string list list
 val zarith_base_modules : string list list
 val init_modules : string list list
 
+(* For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
+
 (*s Global references *)
 
 (* Modules *)