4 files changed, 83 insertions, 5 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 83e866e9f..79060e606 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -391,9 +391,11 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
-\noindent If an inductive constructor or type has arity 2 and the corresponding 
-string is enclosed by parenthesis, then the rest of the string is used
-as infix constructor or type. 
+\noindent When extracting to {\ocaml}, if an inductive constructor or type
+has arity 2 and the corresponding string is enclosed by parentheses,
+and the string meets {\ocaml}'s lexical criteria for an infix symbol,
+then the rest of the string is used as infix constructor or type.
+
 \begin{coq_example}
 Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9cbc3fd71..5d0f9c167 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r)
 
 let pp_modname mp = str (Common.pp_module mp)
 
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+  ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+  [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+(* infix ops in OCaml, but disallowed by preceding grammar *)
+
+let builtin_infixes =
+  [ "::" ; "," ]
+
+let substring_all_opchars s start stop =
+  let rec check_char i =
+    if i >= stop then true
+    else
+      List.mem s.[i] operator_chars && check_char (i+1)
+  in
+  check_char start
+
 let is_infix r =
   is_inline_custom r &&
   (let s = find_custom r in
-   let l = String.length s in
-   l >= 2 && s.[0] == '(' && s.[l-1] == ')')
+   let len = String.length s in
+   len >= 3 &&
+   (* parenthesized *)
+   (s.[0] == '(' && s.[len-1] == ')' &&
+      let inparens = String.trim (String.sub s 1 (len - 2)) in
+      let inparens_len = String.length inparens in
+      (* either, begins with infix symbol, any remainder is all operator chars *)
+      (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
+      (* or, starts with #, at least one more char, all are operator chars *)
+      (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
+      (* or, is an OCaml built-in infix *)
+      (List.mem inparens builtin_infixes)))
 
 let get_infix r =
   let s = find_custom r in
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.