From a2881fa16dccf274a82bbec08ee7b1224df0d1da Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:28:34 +0000
Subject: Newring: replaced some generic = on constr by eq_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14356 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 7f1bf81d19..0df4bed0aa 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -590,10 +590,10 @@ let dest_morph env sigma m_spec =
   match kind_of_term m_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req;
               c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when f = Lazy.force coq_ring_morph ->
+        when eq_constr f (Lazy.force coq_ring_morph) ->
           (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
     | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when f = Lazy.force coq_semi_morph ->
+        when eq_constr f (Lazy.force coq_semi_morph) ->
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
@@ -896,7 +896,7 @@ let dest_field env sigma th_spec =
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when f = Lazy.force field_theory ->
+        when eq_constr f (Lazy.force field_theory) ->
         let rth =
           lapp f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
-- 
cgit v1.2.3