diff options
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3923.v | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/opened/3923.v deleted file mode 100644 index 6aa6b4932e..0000000000 --- a/test-suite/bugs/opened/3923.v +++ /dev/null @@ -1,33 +0,0 @@ -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. - -Fail Extraction MkCertRuntimeTypes. |