diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 17:50:31 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 17:53:51 +0200 |
commit | 5122eb4da3691d32483acd3e481c89d9e5c5c5b9 (patch) | |
tree | 0b6afa891e7497379a4cbb672d8addf97968e956 /kernel/names.ml | |
parent | 981864d47efca1d42f43dc5b7c5439638a86f315 (diff) |
[coqtop] Give priority to stdlib load path over current directory
When initilazing the load path, coqtop adds implicit bindings for stdlib
and for the current directory (-R stdlib Coq -R . ""). In case of
a clash, the binding of the current directory had priority, which makes
it impossible to edit stdlib files (when they Require files from the
same directory) using PG, or from CoqIDE when launched from the directory
containing the file.
Example to reproduce the problem:
```
cd plugins/omega
coqide Omega.v
```
some of the Requires will fail.
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions