From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Sep 2019 11:19:22 +0200
Subject: more proofs going through

---
 common/AST.v    | 1 +
 common/Memory.v | 3 +++
 2 files changed, 4 insertions(+)

(limited to 'common')

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 :=
diff --git a/common/Memory.v b/common/Memory.v
index b68a5049..cfd13601 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -39,6 +39,9 @@ Require Import Values.
 Require Export Memdata.
 Require Export Memtype.
 
+Definition default_notrap_load_value (chunk : memory_chunk) := Vundef.
+
+
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
-- 
cgit