Merge PR #9032: checker: check inductive types by roundtrip through the kernel.

2 files changed, 27 insertions, 0 deletions

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