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")?