diff options
Diffstat (limited to 'test-suite/success/extraction_impl.v')
| -rw-r--r-- | test-suite/success/extraction_impl.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index dfdeff82..a38a688f 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -2,7 +2,9 @@ (** Examples of extraction with manually-declared implicit arguments *) (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) + +Require Coq.extraction.Extraction. (** Bug #4243, part 1 *) @@ -20,9 +22,11 @@ Proof. Defined. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. Extraction Implicit dnat_nat [n]. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. (** Same, with a Fixpoint *) @@ -33,9 +37,11 @@ Fixpoint dnat_nat' n (d:dnat n) := end. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. Extraction Implicit dnat_nat' [n]. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. (** Bug #4243, part 2 *) @@ -54,6 +60,7 @@ Defined. Extraction Implicit es [n]. Extraction Implicit enat_nat [n]. Recursive Extraction enat_nat. +Extraction TestCompile enat_nat. (** Same, with a Fixpoint *) @@ -65,6 +72,7 @@ Fixpoint enat_nat' n (e:enat n) : nat := Extraction Implicit enat_nat' [n]. Recursive Extraction enat_nat'. +Extraction TestCompile enat_nat'. (** Bug #4228 *) @@ -80,3 +88,4 @@ Extraction Implicit two_course [n]. End Food. Recursive Extraction Food.Meal. +Extraction TestCompile Food.Meal. |