Extraction: more cautious use of intermediate result caching (fix #3923)

 During an extraction, a few tables are maintained to cache
 intermediate results. Due to modules, the kernel_name index
 for these caching tables aren't enough. For instance, in
 bug #3923, a constant is first transparent (from inside the
 module) then opaque (when seen from the signature). The previous
 protections were actually obsolete (tests via visible_con), we
 now checks that the constant_body is still the same.

1 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
new file mode 100644
index 000000000..0aa029e73
--- /dev/null
+++ b/test-suite/bugs/closed/3923.v
@@ -0,0 +1,33 @@
+Module Type TRIVIAL.
+Parameter t:Type.
+End TRIVIAL.
+
+Module MkStore (Key : TRIVIAL).
+
+Module St : TRIVIAL.
+Definition t := unit.
+End St.
+
+End MkStore.
+
+
+
+Module Type CERTRUNTIMETYPES (B  : TRIVIAL).
+
+Parameter cert_fieldstore : Type.
+Parameter empty_fieldstore : cert_fieldstore.
+
+End CERTRUNTIMETYPES.
+
+
+
+Module MkCertRuntimeTypes (B  : TRIVIAL) : CERTRUNTIMETYPES B.
+
+Module FieldStore := MkStore B.
+
+Definition cert_fieldstore := FieldStore.St.t.
+Axiom empty_fieldstore : cert_fieldstore.
+
+End MkCertRuntimeTypes.
+
+Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)