diff options
| author | Pierre Boutillier | 2014-09-03 15:18:27 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-09-03 15:18:27 +0200 |
| commit | 1e4a15e74114cef528e76f9aa8b0aeb78e82aecc (patch) | |
| tree | a093f1ac31d37e7b28c84c0617253b90db0e8dc2 /doc/refman/RefMan-ext.tex | |
| parent | d34cb7cc523fe7f6e9b371cee17b7f7b7e588ddf (diff) | |
sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 4 |
1 files changed, 2 insertions, 2 deletions
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. |