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