diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Conventions1.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 045eb471..56beffe8 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -349,8 +349,9 @@ Proof. reflexivity. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** No normalization needed. *) Definition return_value_needs_normalization (t: rettype) := false. +Definition parameter_needs_normalization (t: rettype) := false. |