3 files changed, 41 insertions, 7 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4ae875cd70..c169b7b50b 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+        if mib.mind_finite == CoFinite then raise (I Coinductive);
 	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
 	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 23452febdc..4b6de58bd3 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pcoq.Prim
 
 DECLARE PLUGIN "extraction_plugin"
@@ -42,14 +40,20 @@ ARGUMENT EXTEND int_or_id
 END
 
 let pr_language = function
-  | Ocaml -> str "Ocaml"
+  | Ocaml -> str "OCaml"
   | Haskell -> str "Haskell"
   | Scheme -> str "Scheme"
   | JSON -> str "JSON"
 
+let warn_deprecated_ocaml_spelling =
+  CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+    (fun () ->
+      strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
+| [ "OCaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
 | [ "JSON" ] -> [ JSON ]
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9cbc3fd713..5d0f9c167e 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