diff options
| -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 9265b60c17..704331e784 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. |