From 0f3c1f242ec824a5772c47de61a6cddebe2ee8c8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Nov 2018 14:42:05 +0100
Subject: checker: check inductive types by roundtrip through the kernel.

---
 test-suite/coqchk/inductive_functor_params.v   | 16 ++++++++++++++++
 test-suite/coqchk/inductive_functor_template.v | 11 +++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 test-suite/coqchk/inductive_functor_params.v
 create mode 100644 test-suite/coqchk/inductive_functor_template.v

(limited to 'test-suite')

diff --git a/test-suite/coqchk/inductive_functor_params.v b/test-suite/coqchk/inductive_functor_params.v
new file mode 100644
index 0000000000..f364a62818
--- /dev/null
+++ b/test-suite/coqchk/inductive_functor_params.v
@@ -0,0 +1,16 @@
+
+Module Type T.
+  Parameter foo : nat -> nat.
+End T.
+
+Module F (A:T).
+  Inductive ind (n:nat) : nat -> Prop :=
+  | C : (forall x, x < n -> ind (A.foo n) x) -> ind n n.
+End F.
+
+Module A. Definition foo (n:nat) := n. End A.
+
+Module M := F A.
+(* Note: M.ind could be seen as having 1 recursively uniform
+   parameter, but module substitution does not recognize it, so it is
+   treated as a non-uniform parameter. *)
diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v
new file mode 100644
index 0000000000..bc5cd0fb68
--- /dev/null
+++ b/test-suite/coqchk/inductive_functor_template.v
@@ -0,0 +1,11 @@
+
+Module Type E. Parameter T : Type. End E.
+
+Module F (X:E).
+  #[universes(template)] Inductive foo := box : X.T -> foo.
+End F.
+
+Module ME. Definition T := nat. End ME.
+Module A := F ME.
+(* Note: A.foo could live in Set, and coqchk sees that (because of
+   template polymorphism implementation details) *)
-- 
cgit v1.2.3