I was porting files related to abstract RTA and at some point I created file
task.v in directory
So I've got a situation when I have two files with name
Now, when I try to import
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
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")?