aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/Lagrange.v
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Coqprime/Lagrange.v')
-rw-r--r--coqprime/Coqprime/Lagrange.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v
index b35460bad..b890c5621 100644
--- a/coqprime/Coqprime/Lagrange.v
+++ b/coqprime/Coqprime/Lagrange.v
@@ -14,12 +14,12 @@
Definition: lagrange
**********************************************************************)
-Require Import List.
-Require Import UList.
-Require Import ListAux.
-Require Import ZArith Znumtheory.
-Require Import NatAux.
-Require Import FGroup.
+Require Import Coq.Lists.List.
+Require Import Coqprime.UList.
+Require Import Coqprime.ListAux.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coqprime.NatAux.
+Require Import Coqprime.FGroup.
Open Scope Z_scope.