From f273a85429462e5c81b3e2b81a82f486fe1d94e2 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 3 Nov 2010 12:50:37 +0000
Subject: Correction bug 2427

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

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 12c760ac58..8e74ff7259 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -164,7 +164,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   match mind_of_delta reso2 kn2  with
       | kn2' when kn2=kn2' -> ()
       | kn2' -> 
-	  if not (eq_mind (mind_of_delta reso1 kn1) kn2') then 
+	  if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then 
 	    error ()
   end;
   (* we check that records and their field names are preserved. *)
-- 
cgit v1.2.3