diff options
Diffstat (limited to 'arm/Builtins1.v')
| -rw-r--r-- | arm/Builtins1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Builtins1.v b/arm/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/arm/Builtins1.v +++ b/arm/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. |