diff options
Diffstat (limited to 'powerpc/eabi/Conventions.v')
-rw-r--r-- | powerpc/eabi/Conventions.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/powerpc/eabi/Conventions.v b/powerpc/eabi/Conventions.v index 6e27b9d2..90e14a0a 100644 --- a/powerpc/eabi/Conventions.v +++ b/powerpc/eabi/Conventions.v @@ -792,7 +792,3 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result for dynamic memory allocation *) - -Definition loc_alloc_argument := R3. -Definition loc_alloc_result := R3. |