다른 파일에서 유형 변수를 참조 할 때 오류가 발생했습니다.

나는 coq에서 그룹 이론의 형식화를 연구하고 있습니다. 2 개의 파일이 있습니다.

• groups.v-그룹에 대한 정의 및 정리 포함
• groups_Z.v-Z 그룹에 대한 정리 및 정의를 포함합니다.

groups.v :

Require Import Coq.Setoids.Setoid.
Require Import Coq.Lists.List.
Require Import PeanoNat.

Class Semigroup G : Type :=
{
    mult : G -> G -> G;
    assoc : forall x y z:G,
        mult x (mult y z) = mult (mult x y) z
}.

Class Monoid G `{Hsemi: Semigroup G} : Type :=
{
  e : G;
  left_id : forall x:G, mult e x = x;
}.

Class Group G `{Hmono: Monoid G} : Type :=
{
    inv : G -> G;
    left_inv : forall x:G, mult (inv x) x = e;
}.

Declare Scope group_scope.
Infix "*" := mult (at level 40, left associativity) : group_scope.
Open Scope group_scope.

Section Group_theorems.

  Parameter G: Type.
  Context `{Hgr: Group G}.
  (* More theorems follow *)
  Fixpoint pow (a: G) (n: nat) {struct n} : G :=
    match n with
    | 0 => e
    | S n' => a * (pow a n')
    end.

  Notation "a ** b" := (pow a b) (at level 35, right associativity).

End Group_theorems.
Close Scope group_scope.

groups_Z.v :

Add LoadPath ".".
Require Import groups.
Require Import ZArith.

Open Scope group_scope.
Section Z_Groups.
  Parameter G: Type.
  Context `{Hgr: Group G}.

  Definition pow_z (a: groups.G) (z: Z) : G :=
    match z with
    | Z0 => e
    | Zpos x => pow a (Pos.to_nat x)
    | Zneg x => inv (pow a (Pos.to_nat x))
    end.

  Notation "a ** b" := (pow_z a b) (at level 35, right associativity).
End Z_groups.
Close Scope group_scope.

정의하려는 시도가 다음 pow_z메시지와 함께 실패합니다.

"pow a (Pos.to_nat x)"라는 용어는 "groups.G"유형을 가지며 "G"유형을 가질 것으로 예상됩니다.

다른 서명을 사용하는 경우 : Definition pow_z (a: G) (z: Z) : G

대신 Definition pow_z (a: groups.G) (z: Z) : G.

그런 다음 또 다른 오류가 발생합니다.

용어 "a"는 "G"유형을 가지며 "groups.G"유형을 가질 것으로 예상됩니다.

이 문제를 해결하는 방법?