diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-01-13 11:22:56 -0500 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-01-14 14:39:53 -0500 |
| commit | d3d7622f881956d61e771fecc0b9b0240ff30857 (patch) | |
| tree | 4d4add850dc81727b298ae259760001a1c7e8ca0 /coq/coq-system.el | |
| parent | 27b07f7565013a35d2f1727a5d052078b4262da8 (diff) | |
Add a few comments to explain values of coq-load-path
Diffstat (limited to 'coq/coq-system.el')
| -rw-r--r-- | coq/coq-system.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-system.el b/coq/coq-system.el index 6f49d45f..963a0985 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -174,7 +174,7 @@ coqtop. Usually, the elements of this list are strings (for The possible forms of elements of this list correspond to the 4 forms of include options (`-I' `-Q' and `-R'). An element can be - - A list of the form `(\\='ocamlimport dir)', specifying a + - A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a directory to be added to ocaml path (`-I'). - A list of the form `(\\='rec dir path)' (where dir and path are strings) specifying a directory to be recursively mapped to the @@ -183,7 +183,7 @@ forms of include options (`-I' `-Q' and `-R'). An element can be path are strings) specifying a directory to be recursively mapped to the logical path `path' (`-Q dir path'), but not imported (modules accessible for import with qualified names - only). + only). Note that -Q dir \"\" has a special, nonrecursive meaning. - A list of the form (8.4 only) `(\\='nonrec dir path)', specifying a directory to be mapped to the logical path 'path' ('-I dir -as path'). |