use OCaml criteria for infix ops, #6212

2 files changed, 37 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..35ded8013
--- /dev/null
+++ b/test-suite/output/Extraction_infix.out
@@ -0,0 +1,16 @@
+(** 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
diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v
new file mode 100644
index 000000000..bc0ddb3e1
--- /dev/null
+++ b/test-suite/output/Extraction_infix.v
@@ -0,0 +1,21 @@
+(* @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.