From 5bf13140754a55599ae27942b17cdbb4b7ed74e9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 30 Dec 2012 17:47:53 +0000
Subject: Remove some useless "Require". Update ARM port.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v    | 1 -
 lib/Floats.v    | 2 --
 lib/UnionFind.v | 1 -
 3 files changed, 4 deletions(-)

(limited to 'lib')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 29e65bb..3d5df25 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -21,7 +21,6 @@ Require Export ZArith.
 Require Export Znumtheory.
 Require Export List.
 Require Export Bool.
-Require Import Wf_nat.
 
 (** * Useful tactics *)
 
diff --git a/lib/Floats.v b/lib/Floats.v
index 556cc41..aae2646 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -19,7 +19,6 @@
 Require Import Axioms.
 Require Import Coqlib.
 Require Import Integers.
-Require Import Reals.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
 Require Import Fcore.
@@ -27,7 +26,6 @@ Require Import Fcalc_round.
 Require Import Fcalc_bracket.
 Require Import Fprop_Sterbenz.
 Require Import Program.
-Require Import Omega.
 
 Close Scope R_scope.
 
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 553d905..84d0348 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -15,7 +15,6 @@
 
 (** A persistent union-find data structure. *)
 
-Require Import Wf.
 Require Recdef.
 Require Setoid.
 Require Coq.Program.Wf.
-- 
cgit v1.2.3