Fix doc comment for loc_arguments.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2351 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 6 insertions, 6 deletions

diff --git a/arm/eabi/Conventions1.v b/arm/eabi/Conventions1.v
index 9fc9a50..c02af1a 100644
--- a/arm/eabi/Conventions1.v
+++ b/arm/eabi/Conventions1.v
@@ -256,16 +256,16 @@ Qed.
 
 (** We use the following calling conventions, adapted from the ARM EABI:
 - The first 4 integer arguments are passed in registers [R0] to [R3].
-- The first 2 float arguments are passed in registers [F0] and [F2].
-- The first 4 float arguments are passed in registers [F0] to [F3].
-- The first 2 integer arguments are passed in an aligned pair of two integer
-  registers.
-- Each float argument passed in a float register ``consumes'' an aligned pair
+- The first 2 double float arguments are passed in registers [F0] and [F2].
+- The first 4 single float arguments are passed in registers [F0] to [F3].
+- The first 2 long integer arguments are passed in an aligned pair of
+  two integer registers.
+- Each double argument passed in a float register ``consumes'' an aligned pair
   of two integer registers.
 - Each single argument passed in a float register ``consumes'' an integer
   register.
 - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
-  assigned (1 word for an integer or single argument, 2 words for a float
+  assigned (1 word for an integer or single argument, 2 words for a double
   or a long), starting at word offset 0.
 
 This convention is not quite that of the ARM EABI, whereas every float