diff options
Diffstat (limited to 'test-suite/success/extraction_dep.v')
| -rw-r--r-- | test-suite/success/extraction_dep.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index 11bb25fd..fb0adaba 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -1,8 +1,10 @@ (** Examples of code elimination inside modules during extraction *) +Require Coq.extraction.Extraction. + (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) (** 1) Without signature ... *) @@ -18,6 +20,7 @@ End A. Definition testA := A.u + A.B.x. Recursive Extraction testA. (* without: v w *) +Extraction TestCompile testA. (** 1b) Same with an Include *) @@ -29,6 +32,7 @@ End Abis. Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) +Extraction TestCompile testAbis. (** 2) With signature, we only keep elements mentionned in signature. *) @@ -44,3 +48,4 @@ End Ater. Definition testAter := Ater.u. Recursive Extraction testAter. (* with only: u v *) +Extraction TestCompile testAter. |