From 53b57751c1981e0bce3aa470e426a12034bb165e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Sep 2006 08:58:05 +0000
Subject: Ajout de Init_pointer (experimental)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/AST.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'common/AST.v')

diff --git a/common/AST.v b/common/AST.v
index 673f1d8..5b8c997 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -62,7 +62,8 @@ Inductive init_data: Set :=
   | Init_int32: int -> init_data
   | Init_float32: float -> init_data
   | Init_float64: float -> init_data
-  | Init_space: Z -> init_data.
+  | Init_space: Z -> init_data
+  | Init_pointer: list init_data -> init_data.
 
 (** Whole programs consist of:
 - a collection of function definitions (name and description);
-- 
cgit v1.2.3