diff options
Diffstat (limited to 'doc/refman/RefMan-ide.tex')
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index ec640f4ef..c036f031f 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -120,7 +120,7 @@ insertion cursor. \section{Vernacular commands, templates} -The \texttt{Templates} menu allows to use shortcuts to insert +The \texttt{Templates} menu allows using shortcuts to insert vernacular commands. This is a nice way to proceed if you are not sure of the spelling of the command you want. @@ -193,12 +193,12 @@ will be prompt to choose to either discard your changes or not. The Section~\ref{sec:coqidecharencoding} -The \verb|Externals| section allows to customize the external commands +The \verb|Externals| section allows customizing the external commands for compilation, printing, web browsing. In the browser command, you may use \verb|%s| to denote the URL to open, for example: % \verb|mozilla -remote "OpenURL(%s)"|. -The \verb|Tactics Wizard| section allows to defined the set of tactics +The \verb|Tactics Wizard| section allows defining the set of tactics that should be tried, in sequence, to solve the current goal. The last section is for miscellaneous boolean settings, such as the |