aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/Iterator.v
diff options
context:
space:
mode:
Diffstat (limited to 'coqprime/Coqprime/Iterator.v')
-rw-r--r--coqprime/Coqprime/Iterator.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v
index e84687cd4..96d3e5655 100644
--- a/coqprime/Coqprime/Iterator.v
+++ b/coqprime/Coqprime/Iterator.v
@@ -6,9 +6,9 @@
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
-Require Export Coq.Lists.List.
-Require Export Coqprime.Permutation.
-Require Import Coq.Arith.Arith.
+Require Export List.
+Require Export Permutation.
+Require Import Arith.
Section Iterator.
Variables A B : Set.