coq/ex/test-cases/stale-load-path/b/b.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14

(* This file depends on ../a/Le.v *)

Require Le.

(* The next print should work. *)
Print Le.a.

(* The next print should not work. *)
Print Le.le_refl.


(*** Local Variables: ***)
(*** coq-load-path: ("../a") ***)
(*** End: ***)