From ecfb73d655601e9aed736b0083a6f6b4682a2083 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 22 Nov 2017 12:33:02 -0500
Subject: use OCaml criteria for infix ops, #6212

---
 test-suite/output/Extraction_infix.out | 16 ++++++++++++++++
 test-suite/output/Extraction_infix.v   | 21 +++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 test-suite/output/Extraction_infix.out
 create mode 100644 test-suite/output/Extraction_infix.v

(limited to 'test-suite')

diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out
new file mode 100644
index 0000000000..35ded8013a
--- /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 0000000000..bc0ddb3e16
--- /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.
-- 
cgit v1.2.3


From 79da97a3e02a079e3d91f04fd012886c57d4c1e8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 22 Nov 2017 14:48:04 -0500
Subject: allow whitespace around infix op

---
 test-suite/output/Extraction_infix.out | 4 ++++
 test-suite/output/Extraction_infix.v   | 5 +++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out
index 35ded8013a..29d50775a9 100644
--- a/test-suite/output/Extraction_infix.out
+++ b/test-suite/output/Extraction_infix.out
@@ -14,3 +14,7 @@ let test =
 
 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
index bc0ddb3e16..fe5926a36a 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.
-- 
cgit v1.2.3