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

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

10 files changed, 19 insertions, 9 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ffcb7c648..9f28f819f 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -56,7 +56,7 @@ let tuple_n n =
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
-  Record.definition_structure (false, id, params, fields, cons, mk_Set)
+  Record.definition_structure ((false, id), params, fields, cons, mk_Set)
 
 (*s [(sig_n n)] generates the inductive
     \begin{verbatim}
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index d191b58eb..7bcc3a657 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -229,6 +229,7 @@ let correctness_hook _ ref =
   register pf_id None
 
 let correctness s p opttac =
+  Library.check_required_module ["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 137d12528..7dc6d961f 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -128,6 +128,7 @@ END
 
 (* Guesses the type and calls Field_Gen with the right theory *)
 let field g =
+  Library.check_required_module ["Coq";"field";"Field"];
   let evc = project g
   and env = pf_env g in
   let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
@@ -161,6 +162,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_module ["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 c877dc47b..2cdb929ae 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -395,6 +395,7 @@ let mkAppL a =
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier gl=
+    Library.check_required_module ["Coq";"fourier";"Fourier"];
     let parse = pf_parse_constr gl in
     let goal = strip_outer_cast (pf_concl gl) in
     let fhyp=id_of_string "new_hyp_for_fourier" in
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index a8b965114..1eb22424b 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1860,7 +1860,8 @@ let destructure_goal gl =
 
 let destructure_goal = all_time (destructure_goal)
 
-let omega_solver gl = 
+let omega_solver gl =
+  Library.check_required_module ["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/g_ring.ml4 b/contrib/ring/g_ring.ml4
index e971815b5..a5a02dd76 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -19,7 +19,7 @@ END
 
 (* The vernac commands "Add Ring" and co *)
 
-let cset_of_comarg_list l = 
+let cset_of_constrarg_list l = 
   List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
 
 VERNAC COMMAND EXTEND AddRing
@@ -38,7 +38,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (Some (constr_of aopp))
 			 (constr_of aeq)
 			 (constr_of t)
-			 (cset_of_comarg_list l) ]
+			 (cset_of_constrarg_list l) ]
 
 | [ "Add" "Semi" "Ring" 
       	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
@@ -55,7 +55,7 @@ VERNAC COMMAND EXTEND AddRing
 			 None
 			 (constr_of aeq)
 			 (constr_of t)
-			 (cset_of_comarg_list l) ]
+			 (cset_of_constrarg_list l) ]
 
 | [ "Add" "Abstract" "Ring" 
     	  constr(a) constr(aplus) constr(amult) constr(aone)
@@ -110,7 +110,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (Some (constr_of aopp))
 			 (constr_of aeq)
 			 (constr_of t)
-			 (cset_of_comarg_list l) ]
+			 (cset_of_constrarg_list l) ]
 
 | [ "Add" "Semi" "Setoid" "Ring" 
           constr(a) constr(aequiv) constr(asetth) constr(aplus)
@@ -131,5 +131,5 @@ VERNAC COMMAND EXTEND AddRing
 			 None
 			 (constr_of aeq)
 			 (constr_of t)
-			 (cset_of_comarg_list l) ]
+			 (cset_of_constrarg_list l) ]
 END
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index bcd8ee5f9..c150a4bfb 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -388,7 +388,8 @@ let rec sort_subterm gl l =
   [lc: constr list]\\
   [gl: goal sigma]\\ *)
 
-let quote_terms ivs lc gl= 
+let quote_terms ivs lc gl =
+  Library.check_required_module ["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 25c3f7491..508c1f33e 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -35,7 +35,7 @@ open Nametab
 open Quote
 
 let mt_evd = Evd.empty
-let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
+let constr_of c = Astterm.interp_constr mt_evd (Global.env()) c
 
 let constant dir s =
   let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in
@@ -782,6 +782,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
+  Library.check_required_module ["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, 
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 788d3338c..f87f3db96 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -818,6 +818,7 @@ let destructure_hyps gl =
   loop (pf_ids_of_hyps gl) (pf_hyps gl) gl
 
 let omega_solver gl =
+  Library.check_required_module ["Coq";"romega";"ROmega"];
   let concl = pf_concl gl in
   let rec loop t =
     match destructurate t with
diff --git a/library/library.mli b/library/library.mli
index c29299331..dc34ec72e 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -84,6 +84,8 @@ type library_location = LibLoaded | LibInPath
 val locate_qualified_library :
   Nametab.qualid -> library_location * dir_path * System.physical_path
 
+val check_required_module : string list -> unit
+
 (*s Displays the memory use of a module. *)
 
 val mem : dir_path -> Pp.std_ppcmds