Как импортировать модули в Coq?

У меня проблемы с импортом определений из модулей в Coq. Я новичок в Coq, но не смог решить проблему с помощью справочного руководства по языку или онлайн-руководства. У меня есть модуль, который определяет сигнатуру и аксиомы для конечных множеств, которые я собираюсь реализовать в другом модуле. Есть еще кое-что, но это выглядит примерно так (для справки, я внимательно слежу за статьей Филлиатра о конечных автоматах):

Module FinSet.    
...
Parameter fset     : Set -> Set.
Parameter member   : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union    : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
  forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union    :
  forall A : Set, forall a b : fset A, forall x : A, i
    member x (union a b) <-> (member x a) \/ (member x b).
...
End FinSet.

Я компилирую модуль, используя coqc , и пытаюсь загрузить его в другой модуль. , скажем, FinSetList или FinSetRBT , с помощью команды Требовать импорт FinSet . Когда я пытаюсь импортировать модуль, Coq (через Proof General) выдает предупреждение:

Warning: trying to mask the absolute name "FinSet"!

Кроме того, я не вижу ничего, определенного в FinSet . Как мне импортировать определения (в данном случае аксиомы) из одного модуля в другой? По сути, я следовал шагам, изложенным в лекциях Пирса «Основы программного обеспечения». Однако они не работают на меня.