From cfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Aug 2020 14:41:19 -0400
Subject: [coqchk] Look inside inner modules as well

Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)

I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.

This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
---
 test-suite/output-coqchk/bug_12845.out | 14 ++++++++++++++
 test-suite/output-coqchk/bug_12845.v   | 13 +++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 test-suite/output-coqchk/bug_12845.out
 create mode 100644 test-suite/output-coqchk/bug_12845.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3