From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Floats.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/Floats.v')

diff --git a/lib/Floats.v b/lib/Floats.v
index b95789e6..67b0e53a 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -6,7 +6,6 @@
   and the associated operations.  *)
 
 Require Import Bool.
-Require Import AST.
 Require Import Integers.
 
 Parameter float: Set.
-- 
cgit