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 --- backend/RTL.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index 95fa1f82..29a49311 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -195,8 +195,6 @@ Definition find_function end end. -Definition default_notrap_load_value (chunk : memory_chunk) := Vundef. - (** The transitions are presented as an inductive predicate [step ge st1 t st2], where [ge] is the global environment, [st1] the initial state, [st2] the final state, and [t] the trace -- cgit