aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-11-28 15:45:42 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2017-11-28 15:45:42 -0500
commit6cb9ab00a62b87587b00147d4abd82e684220b03 (patch)
treeaf8d6ef9767e3874021b78b65353271fbb7077e0
parentf228c2eb94346fb3b538d63d95fdd8ab2c0f8795 (diff)
use \ocaml macro in new text
-rw-r--r--doc/refman/Extraction.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index c263ecc48..79060e606 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}