From 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Feb 2020 10:15:40 +0100 Subject: Documentation comment for single_passed_as_single --- powerpc/Archi.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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. -- cgit