diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/bugs/closed/4720.v | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/bugs/closed/4720.v')
-rw-r--r-- | test-suite/bugs/closed/4720.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v new file mode 100644 index 00000000..704331e7 --- /dev/null +++ b/test-suite/bugs/closed/4720.v @@ -0,0 +1,50 @@ +(** Bug 4720 : extraction and "with" in module type *) + +Module Type A. + Parameter t : Set. +End A. + +Module A_instance <: A. + Definition t := nat. +End A_instance. + +Module A_private : A. + Definition t := nat. +End A_private. + +Module Type B. +End B. + +Module Type C (b : B). + Declare Module a : A. +End C. + +Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance). +End WithMod. + +Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat). +End WithDef. + +Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private). +End WithModPriv. + +(* The initial bug report was concerning the extraction of WithModPriv + in Coq 8.4, which was suboptimal: it was compiling, but could have been + turned into some faulty code since A_private and c'.a were not seen as + identical by the extraction. + + In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv + were all causing Anomaly or Assert Failure. This shoud be fixed now. +*) + +Require Extraction. + +Recursive Extraction WithMod. + +Recursive Extraction WithDef. + +Recursive Extraction WithModPriv. + +(* Let's even check that all this extracted code is actually compilable: *) + +Extraction TestCompile WithMod WithDef WithModPriv. |