From d3d142f406239b6e528d27454d1b3f4e3d6fd4ea Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Dec 2018 12:43:23 +0100
Subject: coqchk: fix check for kelim with functors

---
 checker/checkInductive.ml                    |  5 ++++-
 test-suite/coqchk/inductive_functor_squash.v | 15 +++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/coqchk/inductive_functor_squash.v

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index c823db956d..d2d1efcb2c 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -77,6 +77,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> false
 
+let check_kelim k1 k2 =
+  List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1
+
 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost
    the knowledge of who is the canonical version.
    Try with to see test-suite/coqchk/include.v *)
@@ -102,7 +105,7 @@ let check_packet env mind ind
   check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc);
   check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs);
   check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls);
-  check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim);
+  check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim);
 
   check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc);
   (* NB: here syntactic equality is not just an optimisation, we also
diff --git a/test-suite/coqchk/inductive_functor_squash.v b/test-suite/coqchk/inductive_functor_squash.v
new file mode 100644
index 0000000000..9d33fafc4c
--- /dev/null
+++ b/test-suite/coqchk/inductive_functor_squash.v
@@ -0,0 +1,15 @@
+
+
+Module Type T.
+  Parameter f : nat -> Type.
+End T.
+
+Module F(A:T).
+  Inductive ind : Prop :=
+    C : A.f 0 -> ind.
+End F.
+
+Module A. Definition f (x:nat) := True. End A.
+
+Module M := F A.
+(* M.ind could eliminate into Set/Type even though F.ind can't *)
-- 
cgit v1.2.3