diff options
Diffstat (limited to 'test-suite/output/Extraction_infix.v')
| -rw-r--r-- | test-suite/output/Extraction_infix.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v index bc0ddb3e1..fe5926a36 100644 --- a/test-suite/output/Extraction_infix.v +++ b/test-suite/output/Extraction_infix.v @@ -19,3 +19,8 @@ Extraction test. Extract Inductive I => "foo" [ "(@?:::)" ]. Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. |