1 2 3 4 5 6 7 8 9
(* this file depends on b1 and therefore indirectly on ../a/a.v *) Definition a := 2. Require b1. (*** Local Variables: ***) (*** coq-load-path: ("../a") ***) (*** End: ***)