sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex

6 files changed, 20 insertions, 20 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 96b93a8c07..926ee986a7 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -23,7 +23,7 @@ run by the command {\tt coqtop}.
 \index{native code}
 \label{binary-images}
 They are two different binary images of \Coq: the byte-code one and
-the native-code one (if Objective Caml provides a native-code compiler
+the native-code one (if {\ocaml} provides a native-code compiler
 for your platform, which is supposed in the following). By default,
 \verb!coqc! executes the native-code version; this can be overridden
 using the \verb!-byte! option.
@@ -87,7 +87,7 @@ The following command-line options are recognized by the commands {\tt
 \begin{description}
 \item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
 
-Add physical path {\em directory} to the Objective Caml loadpath.
+Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index e594327fab..ef48295150 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1053,12 +1053,12 @@ qualification is recommended.
 There are currently two loadpaths in {\Coq}. There is one loadpath
 where seeking {\Coq} files (extensions \texttt{.v} or \texttt{.vo} or
 \texttt{.vi}) whose management has been explained just above, and one
-where seeking Objective Caml files. The Objective Caml loadpath is
+where seeking {\ocaml} files. The {\ocaml} loadpath is
 managed using the option \texttt{-I path}. As in {\ocaml} world, there
 is nether a notion of logical name prefix nor a way to access files in
 subdirectories of \texttt{path}. See the command \texttt{Declare ML
   Module} in Section~\ref{compiled} to understand the need of the
-Objective Caml loadpath.
+{\ocaml} loadpath.
 
 See Section~\ref{coqoptions} for a more general view over the {\Coq}
 command line options.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index cba664f4c0..bbcb9251da 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1032,7 +1032,7 @@ Inductive Constructions is the one developed as part of the MoWGLI
 European project. It can be found in the file {\tt dev/doc/cic.dtd} of
 the {\Coq} source archive.
 
-An example of parser for this DTD, written in the Objective Caml -
+An example of parser for this DTD, written in the {\ocaml} -
 Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of
 the {\Coq} source archive.
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0c7a534b70..dc5143fd1c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -169,7 +169,7 @@ This command displays the extracted term from
 {\term}. The extraction is processed according to the distinction
 between {\Set} and {\Prop}; that is to say, between logical and
 computational content (see Section~\ref{Sorts}). The extracted term is
-displayed in Objective Caml syntax, where global identifiers are still
+displayed in {\ocaml} syntax, where global identifiers are still
 displayed as in \Coq\ terms.
 
 \begin{Variants}
@@ -680,17 +680,17 @@ This command displays the list of library files loaded in the current
 imported.
 
 \subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}}
-This commands loads the Objective Caml compiled files {\str$_1$} {\ldots}
+This commands loads the {\ocaml} compiled files {\str$_1$} {\ldots}
 {\str$_n$} (dynamic link). It is mainly used to load tactics
 dynamically.
 % (see Chapter~\ref{WritingTactics}).
  The files are
-searched into the current Objective Caml loadpath (see the command {\tt
-Add ML Path} in the Section~\ref{loadpath}).  Loading of Objective Caml
+searched into the current {\ocaml} loadpath (see the command {\tt
+Add ML Path} in the Section~\ref{loadpath}).  Loading of {\ocaml}
 files is only possible under the bytecode version of {\tt coqtop}
 (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
 \ref{Addoc-coqc}), or when Coq has been compiled with a version of
-Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11).
+{\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
 
 \begin{Variants}
 \item {\tt Local Declare ML Module {\str$_1$} .. {\str$_n$}.}\\
@@ -759,16 +759,16 @@ Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirp
 \end{Variants}
 
 \subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}}
-This command adds the path {\str} to the current Objective Caml loadpath (see
+This command adds the path {\str} to the current {\ocaml} loadpath (see
 the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
 \subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}}
 This command adds the directory {\str} and all its subdirectories 
-to the current Objective Caml loadpath (see
+to the current {\ocaml} loadpath (see
 the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 
 \subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
-This command displays the current Objective Caml loadpath.
+This command displays the current {\ocaml} loadpath.
 This command makes sense only under the bytecode version of {\tt
 coqtop}, i.e. using option {\tt -byte} (see the
 command {\tt Declare ML Module} in the section
@@ -874,7 +874,7 @@ This command permits to quit \Coq.
 This is used mostly as a debug facility by \Coq's implementors
 and does not concern the casual user.
 This command permits to leave {\Coq} temporarily and enter the
-Objective Caml toplevel. The Objective Caml command:
+{\ocaml} toplevel. The {\ocaml} command:
 
 \begin{flushleft}
 \begin{verbatim}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 1e83bd956b..23d4ee10d8 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -201,7 +201,7 @@ Gérard Huet
 %\addcontentsline{toc}{section}{Credits: addendum for version V6.1}
 
 The present version 6.1 of \Coq{} is based on the V5.10 architecture. It
-was ported to the new language Objective Caml by Bruno Barras. The
+was ported to the new language {\ocaml} by Bruno Barras. The
 underlying framework has slightly changed and allows more conversions
 between sorts. 
 
@@ -564,7 +564,7 @@ unresolved implicit has been implemented by Hugo Herbelin.
 Laurent Théry's contribution on strings and Pierre Letouzey and
 Jean-Christophe Filliâtre's contribution on finite maps have been
 integrated to the {\Coq} standard library. Pierre Letouzey developed a
-library about finite sets ``à la Objective Caml''. With Jean-Marc
+library about finite sets ``à la {\ocaml}''. With Jean-Marc
 Notin, he extended the library on lists. Pierre Letouzey's
 contribution on rational numbers has been integrated and extended..
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 5d956ad719..2b852d5f41 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -6,8 +6,8 @@ beside proof development, tactics writing or documentation.
 \section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}}
 
 The native-code version of \Coq\ cannot dynamically load user tactics
-using Objective Caml code. It is possible to build a toplevel of \Coq,
-with Objective Caml code statically linked, with the tool {\tt
+using {\ocaml} code. It is possible to build a toplevel of \Coq,
+with {\ocaml} code statically linked, with the tool {\tt
   coqmktop}.
 
 For example, one can build a native-code \Coq\ toplevel extended with a tactic
@@ -24,10 +24,10 @@ A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
 which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
 
 
-\paragraph[Application: how to use the Objective Caml debugger with Coq.]{Application: how to use the Objective Caml debugger with Coq.\index{Debugger}}
+\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}}
 
 One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
-order to debug your tactics with the Objective Caml debugger.
+order to debug your tactics with the {\ocaml} debugger.
 You need to have configured and compiled \Coq\ for debugging
 (see the file \texttt{INSTALL} included in the distribution).
 Then, you must compile the Caml modules of your tactic with the