Revu traitement des variables globales dans AST.program et dans Globalenvs.

Adaptation frontend, backend en consequence.
Integration passe C -> C#minor dans common/Main.v.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1 insertions, 16 deletions

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index d3bd8d6f..979d0bca 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -130,11 +130,7 @@ Inductive fundef : Set :=
 
 (** Program *)
 
-Record program : Set := mkprogram {
-    prog_funct: list (ident * fundef);
-    prog_defs: list (ident * type * list init_data);
-    prog_main: ident
-}.
+Definition program : Set := AST.program fundef type.
 
 (** ** Operations over types *)
 
@@ -293,17 +289,6 @@ Definition access_mode (ty: type) : mode :=
   | Tunion fList => By_nothing
 end.
 
-(** Conversion of a Clight program into an AST program *)
-
-Definition extract_global_var (id_ty_init: ident * type * list init_data) :=
-  match id_ty_init with (id, ty, init) => (id, init) end.
-
-Definition program_of_program (p: program) : AST.program fundef :=
-  AST.mkprogram
-    p.(prog_funct)
-    p.(prog_main)
-    (List.map extract_global_var p.(prog_defs)).
-
 (** Classification of arithmetic operations and comparisons *)
 
 Inductive classify_add_cases : Set :=