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

3 files changed, 9 insertions, 7 deletions

diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index e971815b54..a5a02dd76c 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 bcd8ee5f94..c150a4bfb6 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 25c3f74917..508c1f33e6 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,