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

---
 test-suite/coqchk/inductive_functor_squash.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/coqchk/inductive_functor_squash.v

(limited to 'test-suite')

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