aboutsummaryrefslogtreecommitdiff
path: root/coqprime/Coqprime/Permutation.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-03-10 13:45:37 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-03-10 13:45:37 -0500
commitdbe09dd5bfc2595cb9fd96725d87d9a729cd0247 (patch)
tree0e6fd0aec064ee4ec2de47ccbbfcd6abecf9a75d /coqprime/Coqprime/Permutation.v
parent003f348b0b69236309467d8e543c4da2c853de1b (diff)
Absolutize Coqprime imports
Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ```
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 a06693f89..7cb6f629d 100644
--- a/coqprime/Coqprime/Permutation.v
+++ b/coqprime/Coqprime/Permutation.v
@@ -11,8 +11,8 @@
Defintion and properties of permutations
**********************************************************************)
-Require Export List.
-Require Export ListAux.
+Require Export Coq.Lists.List.
+Require Export Coqprime.ListAux.
Section permutation.
Variable A : Set.