(* this file depends on a.v and b.v *)

Require Import a b.

Definition a := 3.