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(-)

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