diff options
Diffstat (limited to 'common/Memtype.v')
| -rw-r--r-- | common/Memtype.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/common/Memtype.v b/common/Memtype.v index a13e861..b7d953f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -418,7 +418,6 @@ Axiom load_store_similar: Axiom load_store_same: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - Val.has_type v (type_of_chunk chunk) -> load chunk m2 b ofs = Some (Val.load_result chunk v). Axiom load_store_other: |