Merge PR #12862: [coqchk] Look inside inner modules as well

Reviewed-by: ppedrot
Reviewed-by: proux01

2 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/output-coqchk/bug_12845.out b/test-suite/output-coqchk/bug_12845.out
new file mode 100644
index 0000000000..bef45bf2f6
--- /dev/null
+++ b/test-suite/output-coqchk/bug_12845.out
@@ -0,0 +1,14 @@
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+  
+* Axioms: <none>
+  
+* Constants/Inductives relying on type-in-type: <none>
+  
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+  
+* Inductives whose positivity is assumed: <none>
+  
diff --git a/test-suite/output-coqchk/bug_12845.v b/test-suite/output-coqchk/bug_12845.v
new file mode 100644
index 0000000000..d16146855b
--- /dev/null
+++ b/test-suite/output-coqchk/bug_12845.v
@@ -0,0 +1,13 @@
+Module Type A.
+  Module B.
+    Axiom t : Set.
+  End B.
+End A.
+
+Module a : A.
+  Module B.
+    Definition t : Set := unit.
+  End B.
+End a.
+
+Check a.B.t.