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/refman/Extraction.tex')

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


From 6cb9ab00a62b87587b00147d4abd82e684220b03 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 28 Nov 2017 15:45:42 -0500
Subject: use \ocaml macro in new text

---
 doc/refman/Extraction.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/Extraction.tex')

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index c263ecc486..79060e6062 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -391,9 +391,9 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
-\noindent When extracting to Ocaml, if an inductive 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,
+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}
-- 
cgit v1.2.3

