diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Conventions1.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 3bd2b553..b94ce9ef 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -436,8 +436,9 @@ Proof. destruct Archi.abi; 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. |