diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
commit | 2ae7674c6788742c021988ac02caabceec958957 (patch) | |
tree | 8f8c17a32a4a77ace1eac05760847c8c12d35670 /test-suite/output | |
parent | 14c041012bd375cae018f83d107c836fca3d1f01 (diff) | |
parent | 6cb9ab00a62b87587b00147d4abd82e684220b03 (diff) |
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Extraction_infix.out | 20 | ||||
-rw-r--r-- | test-suite/output/Extraction_infix.v | 26 |
2 files changed, 46 insertions, 0 deletions
diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 000000000..29d50775a --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,20 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False +(** val test : foo **) + +let test = + True @?::: False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 000000000..fe5926a36 --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,26 @@ +(* @herbelin's example for issue #6212 *) + +Require Import Extraction. +Inductive I := C : bool -> bool -> I. +Definition test := C true false. + +(* the parentheses around the function wrong signalled an infix operator *) + +Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ]. +Extraction test. + +(* some bonafide infix operators *) + +Extract Inductive I => "foo" [ "(@@?)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(#^^)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(@?:::)" ]. +Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. |