From d358d9de3afbc1adf28e6cda48ef081a07cb6e76 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 30 May 2013 12:52:25 +0000
Subject: bwaa, a Pervasive.compare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16542 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5817357362..2109ba632f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -30,7 +30,7 @@ module Refset' = Refset_env
 
 let occur_kn_in_ref kn = function
   | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> kn = kn'
+  | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
 
-- 
cgit v1.2.3