aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/EGroup.v
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Coqprime/EGroup.v')
-rw-r--r--coqprime/Coqprime/EGroup.v18
1 files changed, 9 insertions, 9 deletions
diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v
index fd543fe04..553cb746c 100644
--- a/coqprime/Coqprime/EGroup.v
+++ b/coqprime/Coqprime/EGroup.v
@@ -11,15 +11,15 @@
Given an element a, create the group {e, a, a^2, ..., a^n}
**********************************************************************)
-Require Import ZArith.
-Require Import Tactic.
-Require Import List.
-Require Import ZCAux.
-Require Import ZArith Znumtheory.
-Require Import Wf_nat.
-Require Import UList.
-Require Import FGroup.
-Require Import Lagrange.
+Require Import Coq.ZArith.ZArith.
+Require Import Coqprime.Tactic.
+Require Import Coq.Lists.List.
+Require Import Coqprime.ZCAux.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Arith.Wf_nat.
+Require Import Coqprime.UList.
+Require Import Coqprime.FGroup.
+Require Import Coqprime.Lagrange.
Open Scope Z_scope.