diff options
Diffstat (limited to 'test-suite/success/extraction_polyprop.v')
| -rw-r--r-- | test-suite/success/extraction_polyprop.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v index 7215bd99..936d838c 100644 --- a/test-suite/success/extraction_polyprop.v +++ b/test-suite/success/extraction_polyprop.v @@ -3,6 +3,8 @@ code that segfaults. See Table.error_singleton_become_prop or S. Glondu's thesis for more details. *) +Require Coq.extraction.Extraction. + Definition f {X} (p : (nat -> X) * True) : X * nat := (fst p 0, 0). |