Newring: generic equality on constr replaced by constr_equal

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

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 38c65cdd0..e63dbba42 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -574,13 +574,13 @@ let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
   match kind_of_term th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when f = Lazy.force coq_almost_ring_theory ->
+        when eq_constr f (Lazy.force coq_almost_ring_theory) ->
           (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
-        when f = Lazy.force coq_semi_ring_theory ->
+        when eq_constr f (Lazy.force coq_semi_ring_theory) ->
         (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when f = Lazy.force coq_ring_theory ->
+        when eq_constr f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"