diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-26 20:00:07 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-07-26 20:01:06 +0200 |
| commit | 324a90078a47e469e4b185cfc6333a741cf48dc2 (patch) | |
| tree | 71724e024f1156741ddd1d9bd73dbe1033b38112 /test-suite | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Enrich test file 4720.v with a compilation test of the extracted code
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4720.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v index 9265b60c1..704331e78 100644 --- a/test-suite/bugs/closed/4720.v +++ b/test-suite/bugs/closed/4720.v @@ -44,3 +44,7 @@ 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. |