aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v
blob: 6d79572a8002605dce05e23d9c2af3583ba5b2fa (plain)
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: ***)