From a6c1292b72cebf3d34a0e6a2da256e83e346dacc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 31 Oct 2018 14:29:39 +0100
Subject: Fix #8881: validate fails to use inductive equivalence in case_info

See also 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b
---
 checker/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5e34f04f51..269a98cb0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -388,7 +388,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let mib, mip as spec = lookup_mind_specif env indsp in
   if
-    not (eq_ind_chk indsp ci.ci_ind) ||
+    not (mind_equiv env indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
     (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
-- 
cgit v1.2.3