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

---
 doc/refman/Extraction.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 83e866e9f3..c263ecc486 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 => "(*)"  [ "(,)" ].
-- 
cgit v1.2.3