Getting rid of the previous implementation of setoid_rewrite which was

unplugged a long time ago.


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

3 files changed, 12 insertions, 16 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6b65fbcc5f..68460c76e1 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1906,7 +1906,6 @@ let rec xlate_vernac =
 	    xlate_error "TODO: Print TypeClasses"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
-	| PrintSetoids -> CT_print_setoids
 	| PrintTables -> CT_print_tables
         | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
         | PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index eac109cae8..adcf51fe85 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -307,14 +307,14 @@ let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
 let implement_theory env t th args =
   is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))
 
-(* The following test checks whether the provided morphism is the default
-   one for the given operation. In principle the test is too strict, since
-   it should possible to provide another proof for the same fact (proof
-   irrelevance). In particular, the error message is be not very explicative. *)
+(* (\* The following test checks whether the provided morphism is the default *)
+(*    one for the given operation. In principle the test is too strict, since *)
+(*    it should possible to provide another proof for the same fact (proof *)
+(*    irrelevance). In particular, the error message is be not very explicative. *\) *)
 let states_compatibility_for env plus mult opp morphs =
- let check op compat =
-  is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem
-   compat in
+ let check op compat = true in
+(*   is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *)
+(*    compat in *)
  check plus morphs.plusm &&
  check mult morphs.multm &&
  (match (opp,morphs.oppm) with
@@ -826,12 +826,10 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS
 		 (tclORELSE
-                   (Setoid_replace.general_s_rewrite true
-		     Termops.all_occurrences c'i_eq_c''i
-                     ~new_goals:[])
-                   (Setoid_replace.general_s_rewrite false 
-		     Termops.all_occurrences c'i_eq_c''i
-                     ~new_goals:[]))
+                   (Equality.general_rewrite true
+		     Termops.all_occurrences c'i_eq_c''i)
+                   (Equality.general_rewrite false 
+		     Termops.all_occurrences c'i_eq_c''i))
                  [tac]))
 	 else
            (tclORELSE
@@ -881,7 +879,7 @@ let guess_equiv_tac th =
 
 let match_with_equiv c = match (kind_of_term c) with
   | App (e,a) -> 
-      if (List.mem e (Setoid_replace.equiv_list ()))
+      if (List.mem e []) (*  (Setoid_replace.equiv_list ())) *)
       then Some (decompose_app c)
       else None
   | _ -> None
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index fc66b1c971..617ee4bed4 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -25,7 +25,6 @@ open Tacexpr
 open Pcoq
 open Tactic
 open Constr
-open Setoid_replace
 open Proof_type
 open Coqlib
 open Tacmach