Nettoyage et documentation de Library

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

8 files changed, 9 insertions, 9 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 9dce63191..98ea8e495 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -232,7 +232,7 @@ let discriminate_tac axioms cstr p gls =
 (* wrap everything *)
 	
 let cc_tactic gls=
-  Library.check_required_library ["Coq";"Init";"Logic"];
+  Coqlib.check_required_library ["Coq";"Init";"Logic"];
   let (axioms,disaxioms,glo)=make_prb gls in
     match (cc_proof axioms disaxioms glo) with
         `Prove_goal p -> proof_tac axioms p gls
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index bb6e33011..bd742b9df 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -234,7 +234,7 @@ let correctness_hook _ ref =
   register pf_id None
 
 let correctness s p opttac =
-  Library.check_required_library ["Coq";"correctness";"Correctness"];
+  Coqlib.check_required_library ["Coq";"correctness";"Correctness"];
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
   let env = Global.env () in
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 94044cf20..9f887fc75 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -150,7 +150,7 @@ END
 
 (* Guesses the type and calls field_gen with the right theory *)
 let field g =
-  Library.check_required_library ["Coq";"field";"Field"];
+  Coqlib.check_required_library ["Coq";"field";"Field"];
   let ist = { lfun=[]; debug=get_debug () } in
   let typ = 
     match Hipattern.match_with_equation (pf_concl g) with
@@ -173,7 +173,7 @@ let guess_theory env evc = function
 
 (* Guesses the type and calls Field_Term with the right theory *)
 let field_term l g =
-  Library.check_required_library ["Coq";"field";"Field"];
+  Coqlib.check_required_library ["Coq";"field";"Field"];
   let env = (pf_env g)
   and evc = (project g) in
   let th = valueIn (VConstr (guess_theory env evc l))
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 33d6faad1..5e31d5675 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -458,7 +458,7 @@ let mkAppL a =
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier gl=
-    Library.check_required_library ["Coq";"fourier";"Fourier"];
+    Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = strip_outer_cast (pf_concl gl) in
     let fhyp=id_of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 6a99aedc8..a6a8937ba 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -401,7 +401,7 @@ let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
       (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
-      read_library (dummy_loc,qid);
+      require_library [dummy_loc,qid] None;
       msg (str "opening... ");
       Declaremods.import_module false (Nametab.locate_module qid); 
       msgnl (str "done" ++ fnl ());
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 1e02f23b5..41eec8dc8 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1785,7 +1785,7 @@ let destructure_goal gl =
 let destructure_goal = all_time (destructure_goal)
 
 let omega_solver gl =
-  Library.check_required_library ["Coq";"omega";"Omega"];
+  Coqlib.check_required_library ["Coq";"omega";"Omega"];
   let result = destructure_goal gl in 
   (* if !display_time_flag then begin text_time (); 
      flush Pervasives.stdout end; *)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 5a381b57c..fb0e66526 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -385,7 +385,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Library.check_required_library ["Coq";"ring";"Quote"];
+  Coqlib.check_required_library ["Coq";"ring";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 384784fdc..d3068c862 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -885,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
-  Library.check_required_library ["Coq";"ring";"Ring"];
+  Coqlib.check_required_library ["Coq";"ring";"Ring"];
   match lc with 
    (* If no argument is given, try to recognize either an equality or
       a declared relation with arguments c1 ... cn,