diff options
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/4720.v | 46 | ||||
-rw-r--r-- | test-suite/bugs/closed/5177.v | 21 |
2 files changed, 67 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v new file mode 100644 index 000000000..9265b60c1 --- /dev/null +++ b/test-suite/bugs/closed/4720.v @@ -0,0 +1,46 @@ +(** 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. diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v new file mode 100644 index 000000000..231d103a5 --- /dev/null +++ b/test-suite/bugs/closed/5177.v @@ -0,0 +1,21 @@ +(* Bug 5177 https://coq.inria.fr/bug/5177 : + Extraction and module type containing application and "with" *) + +Module Type T. + Parameter t: Type. +End T. + +Module Type A (MT: T). + Parameter t1: Type. + Parameter t2: Type. + Parameter bar: MT.t -> t1 -> t2. +End A. + +Module MakeA(MT: T): A MT with Definition t1 := nat. + Definition t1 := nat. + Definition t2 := nat. + Definition bar (m: MT.t) (x:t1) := x. +End MakeA. + +Require Extraction. +Recursive Extraction MakeA. |