diff options
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 94a9917..20c0b10 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -103,19 +103,6 @@ Proof. destruct chunk1; destruct chunk2; simpl; congruence. Qed. -(** The type (integer/pointer or float) of a chunk. *) - -Definition type_of_chunk (c: memory_chunk) : typ := - match c with - | Mint8signed => Tint - | Mint8unsigned => Tint - | Mint16signed => Tint - | Mint16unsigned => Tint - | Mint32 => Tint - | Mfloat32 => Tfloat - | Mfloat64 => Tfloat - end. - (** * Memory values *) (** A ``memory value'' is a byte-sized quantity that describes the current |