From ddcc36cc2ef44a40a2f636f1096c63f4043c8959 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:27:13 +0000
Subject: 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
---
 plugins/setoid_ring/newring.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 38c65cdd09..e63dbba42a 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"
 
-- 
cgit v1.2.3