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

1 files changed, 0 insertions, 1 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index b95789e..67b0e53 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.