diff options
Diffstat (limited to 'powerpc/Archi.v')
| -rw-r--r-- | powerpc/Archi.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 88fff302..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,7 +30,8 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. -(** Should singles be passed as single or double *) +(** Should single-precision FP arguments passed on stack be passed + as singles or use double FP format. *) Parameter single_passed_as_single : bool. Definition splitlong := negb ppc64. |