Merge PR #9250: coqchk: fix check for kelim with functors

Ack-by: mattam82
Reviewed-by: ppedrot

1 files changed, 15 insertions, 0 deletions

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 *)