Remove commented-out code

1 files changed, 0 insertions, 53 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 3b44c34303..76c393450b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -425,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph r add mul req m1 m2 =
   lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
 
-(* let default_ring_equality (r,add,mul,opp,req) = *)
-(*   let is_setoid = function *)
-(*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(*         eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
-(*     | _ -> false in *)
-(*   match default_relation_for_carrier ~filter:is_setoid r with *)
-(*       Leibniz _ -> *)
-(*         let setoid = lapp coq_eq_setoid [|r|] in *)
-(*         let op_morph = *)
-(*           match opp with *)
-(*               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
-(*             | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
-(*         (setoid,op_morph) *)
-(*     | Relation rel -> *)
-(*         let setoid = setoid_of_relation rel in *)
-(*         let is_endomorphism = function *)
-(*             { args=args } -> List.for_all *)
-(*                 (function (var,Relation rel) -> *)
-(*                   var=None && eq_constr_nounivs req rel *)
-(*                   | _ -> false) args in *)
-(*         let add_m = *)
-(*           try default_morphism ~filter:is_endomorphism add *)
-(*           with Not_found -> *)
-(*             error "ring addition should be declared as a morphism" in *)
-(*         let mul_m = *)
-(*           try default_morphism ~filter:is_endomorphism mul *)
-(*           with Not_found -> *)
-(*             error "ring multiplication should be declared as a morphism" in *)
-(*         let op_morph = *)
-(*           match opp with *)
-(*             | Some opp -> *)
-(*             (let opp_m = *)
-(*               try default_morphism ~filter:is_endomorphism opp *)
-(*               with Not_found -> *)
-(*                 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 *)
-(*                (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++   *)
-(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(*                str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
-(*                str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
-(*                str"\""); *)
-(*              op_morph) *)
-(*             | None -> *)
-(*             (msgnl *)
-(*               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++   *)
-(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(*                str"\""++spc()++str"and \""++ *)
-(*                pr_constr mul_m.morphism_theory++str"\""); *)
-(*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
-(*         (setoid,op_morph) *)
-
 let ring_equality env evd (r,add,mul,opp,req) =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->