aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Sets.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-11-11 14:24:33 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-11-11 14:24:33 +0000
commita3bc7b24d5f21b99a37a529d06707c5f0e550679 (patch)
treeb450c9693449e7f080ae3f0f9707ffa89e2f0f89 /lib/Sets.v
parent7a3338431e5f09a90bfda16350202f5c7780d110 (diff)
downloadcompcert-a3bc7b24d5f21b99a37a529d06707c5f0e550679.tar.gz
compcert-a3bc7b24d5f21b99a37a529d06707c5f0e550679.zip
Petites adaptations pour Coq 8.1gamma
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Sets.v')
-rw-r--r--lib/Sets.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/Sets.v b/lib/Sets.v
index bfc49b11..0a809fcd 100644
--- a/lib/Sets.v
+++ b/lib/Sets.v
@@ -9,7 +9,6 @@
implementation of sets.
*)
-Require Import Relations.
Require Import Coqlib.
Require Import Maps.
Require Import Lattice.