Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in case_info

2 files changed, 24 insertions, 1 deletions

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) ||
diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v
new file mode 100644
index 0000000000..dfc209b318
--- /dev/null
+++ b/test-suite/coqchk/bug_8881.v
@@ -0,0 +1,23 @@
+
+(* Check use of equivalence on inductive types (bug #1242) *)
+
+Module Type ASIG.
+  Inductive t : Set := a | b : t.
+  Definition f := fun x => match x with a => true | b => false end.
+End ASIG.
+
+Module Type BSIG.
+  Declare Module A : ASIG.
+  Definition f := fun x => match x with A.a => true | A.b => false end.
+End BSIG.
+
+Module C (A : ASIG) (B : BSIG with Module A:=A).
+
+  (* Check equivalence is considered in "case_info" *)
+  Lemma test : forall x, A.f x = B.f x.
+  Proof.
+    intro x. unfold B.f, A.f.
+    destruct x; reflexivity.
+  Qed.
+
+End C.