diff options
| author | pboutill | 2010-05-18 15:57:21 +0000 |
|---|---|---|
| committer | pboutill | 2010-05-18 15:57:21 +0000 |
| commit | faa0de5c67594980f8ad871dcf71c0dc98865a5e (patch) | |
| tree | a95bd8204fbdeb0925ab64bd15992d4c35ce6f17 /doc | |
| parent | e7c9f5f130f5187e5d9b43c8f0ed15deb49e4b2c (diff) | |
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 824943d47d..f808047b12 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -58,12 +58,14 @@ native-code versions of the system. \section[Resource file]{Resource file\index{Resource file}} When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the -resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is -the home directory of the user. If this file is not found, then the -file \verb:$HOME/.coqrc: is searched. You can also specify an -arbitrary name for the resource file (see option \verb:-init-file: -below), or the name of another user to load the resource file of -someone else (see option \verb:-user:). +resource file \verb:$HOME/.coqrc.xxx: is loaded, where \verb:$HOME: is +the home directory of the user and \verb:xxx: is the version number +(e.g. 8.3). If this file is not found, then the file +\verb:$HOME/.coqrc: is searched. You can also specify an arbitrary +name for the resource file (see option \verb:-init-file: below), or +the name of another user to load the resource file of someone else +(see option \verb:-user:). + This file may contain, for instance, \verb:Add LoadPath: commands to add directories to the load path of \Coq. |