(* test file *)

theory A
  type t
  axiom Ax : forall x:t. true
end

theory B
  use A
  use A
end