aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/Permutation.v
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Coqprime/Permutation.v')
-rw-r--r--coqprime/Coqprime/Permutation.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v
index 7cb6f629d..a06693f89 100644
--- a/coqprime/Coqprime/Permutation.v
+++ b/coqprime/Coqprime/Permutation.v
@@ -11,8 +11,8 @@
Defintion and properties of permutations
**********************************************************************)
-Require Export Coq.Lists.List.
-Require Export Coqprime.ListAux.
+Require Export List.
+Require Export ListAux.
Section permutation.
Variable A : Set.