aboutsummaryrefslogtreecommitdiffstats
path: root/common/AST.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/AST.v')
-rw-r--r--common/AST.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/common/AST.v b/common/AST.v
index d98f954a..bb8508b7 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -202,6 +202,7 @@ Proof.
decide equality.
Defined.
+
(** Initialization data for global variables. *)
Inductive init_data: Type :=