diff options
Diffstat (limited to 'arm/linux/Conventions.v')
| -rw-r--r-- | arm/linux/Conventions.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/arm/linux/Conventions.v b/arm/linux/Conventions.v index 03425213..a35162c2 100644 --- a/arm/linux/Conventions.v +++ b/arm/linux/Conventions.v @@ -852,7 +852,3 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result for dynamic memory allocation *) - -Definition loc_alloc_argument := R0. -Definition loc_alloc_result := R0. |