aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/multiple-files-single-dir/e.v
blob: 9dc2be323fb5852fd5d5b96d114950a014d76a29 (plain)
1
2
3
4
5
(* this file depends on b.v and c.v *)

Require Import b c.

Definition a := 4.