diff options
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/common/AST.v b/common/AST.v index 6f35be0..29d1452 100644 --- a/common/AST.v +++ b/common/AST.v @@ -586,9 +586,9 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default + | EF_vstore chunk => mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk_use chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default |