Removed unneeded tactics from RelationClasses. Use

check_required_library where needed (fixes bug #1797). 
Remove spurious messages from ring when not in verbose mode.


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

5 files changed, 22 insertions, 15 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 6ed79f23b..7cf642ce7 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -545,19 +545,21 @@ let ring_equality (r,add,mul,opp,req) =
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
-		  msgnl
+		  Flags.if_verbose 
+		    msgnl
 		    (str"Using setoid \""++pr_constr req++str"\""++spc()++  
-			str"and morphisms \""++pr_constr add_m ++
-			str"\","++spc()++ str"\""++pr_constr mul_m++
-			str"\""++spc()++str"and \""++pr_constr opp_m++
+			str"and morphisms \""++pr_constr add_m_lem ++
+			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
+			str"\""++spc()++str"and \""++pr_constr opp_m_lem++
 			str"\"");
 		  op_morph)
             | None ->
-		(msgnl
+		(Flags.if_verbose
+		    msgnl
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++  
-			str"and morphisms \""++pr_constr add_m ++
+			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
-			pr_constr mul_m++str"\"");
+			pr_constr mul_m_lem++str"\"");
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 	    
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 2d1be640b..e7a727bb5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -112,10 +112,7 @@ let vernac_assumption env isevars kind l nl =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-(*   check_required_library ["Coq";"Logic";"JMeq"]; *)
-  require_library "Coq.Program.Wf";
-  require_library "Coq.Program.Tactics";
-  require_library "Coq.Logic.JMeq";
+  check_required_library ["Coq";"Program";"Tactics"];
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e46ca822e..54ed30a5d 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1586,7 +1586,8 @@ let eq_id avoid id =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq typ x typ' y = 
+  mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
 let hole = RHole (dummy_loc, Evd.QuestionMark true)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 9c40c861e..a8bc546aa 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -176,6 +176,7 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with
   | _ -> assert(false)
 
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+  Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index b684dd320..dc79597dd 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -64,9 +64,15 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
 
-let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_ind =   
+  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
+	init_constant ["Logic";"JMeq"] "JMeq")
+let jmeq_rec = 
+  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
+	init_constant ["Logic";"JMeq"] "JMeq_rec")
+let jmeq_refl = 
+  lazy (check_required_library ["Coq";"Logic";"JMeq"];
+	init_constant ["Logic";"JMeq"] "JMeq_refl")
 
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")