Ambiguous-file-name warning
I was porting files related to abstract RTA and at some point I created file task.v
in directory model/preemption/
.
So I've got a situation when I have two files with name task
-- model/task.v
and model/preemption/task.v
.
Now, when I try to import model/task.v
via
From rt.restructuring.model Require Import task
I see the following warning. Moreover, as you can see, Coq loads file model/preemption/task.v
instead of model/task.v
.
Warning: task.vo has been found in
[ ./rt-proofs/restructuring/model/preemption ;
./rt-proofs/restructuring/model ];
loading ./rt-proofs/restructuring/model/preemption/task.vo
[ambiguous-file-name,filesystem]
One solution I see is replacing From rt.restructuring.model Require Import task
with From rt.restructuring Require Import model.task
.
But is it possible to fix this problem in a more solid way (e.g. make imports more "conservative")?