diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-24 09:10:35 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-24 09:10:35 +0000 |
| commit | 75fea20a8289e4441819b45d7ce750eda1b53ad1 (patch) | |
| tree | 5f425efb2ee4b5f5fa263c067f5491e3ff8736c2 /common/Events.v | |
| parent | c7099a26a0b5fd13987454fbe9a56e2b2d711726 (diff) | |
Type-checking of builtin volatile write Mfloat32 was too strict, causing type errors after optimization.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2434 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/common/Events.v b/common/Events.v index 8b6d25f..48cd91e 100644 --- a/common/Events.v +++ b/common/Events.v @@ -967,7 +967,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1022,7 +1022,7 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default). + (mksignature (type_of_chunk_use chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) |