From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Sep 2019 11:19:22 +0200 Subject: more proofs going through --- common/Memory.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'common/Memory.v') 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