aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-19 17:50:31 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-19 17:53:51 +0200
commit5122eb4da3691d32483acd3e481c89d9e5c5c5b9 (patch)
tree0b6afa891e7497379a4cbb672d8addf97968e956 /pretyping
parent981864d47efca1d42f43dc5b7c5439638a86f315 (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 'pretyping')
0 files changed, 0 insertions, 0 deletions