aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/IGroup.v
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Coqprime/IGroup.v')
-rw-r--r--coqprime/Coqprime/IGroup.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v
index 04219be5a..11a73d414 100644
--- a/coqprime/Coqprime/IGroup.v
+++ b/coqprime/Coqprime/IGroup.v
@@ -13,12 +13,12 @@
Definition: ZpGroup
**********************************************************************)
-Require Import Coq.ZArith.ZArith.
-Require Import Coqprime.Tactic.
-Require Import Coq.Arith.Wf_nat.
-Require Import Coqprime.UList.
-Require Import Coqprime.ListAux.
-Require Import Coqprime.FGroup.
+Require Import ZArith.
+Require Import Tactic.
+Require Import Wf_nat.
+Require Import UList.
+Require Import ListAux.
+Require Import FGroup.
Open Scope Z_scope.