Hide annotations on procedures.

[xorque <xorquewasp@googlemail.com>]

Having failed to take the day off from learning SPARK, I've run into
a strange problem regarding procedure annotations.

I have the following in a package body:

  procedure C_Readlink_Boundary
    (File_Name     : in String;
     Buffer        : out String;
     Buffer_Size   : in File.File_Name_Index_t;
     Returned_Size : out C_Types.Signed_Size_t)
  is
    --# hide C_Readlink_Boundary
  begin
    null;
  end C_Readlink_Boundary;

The body of the procedure is obviously not implemented yet. The
procedure
itself is defined only in the body of the package, not accessible from
outside.
The body of the procedure is intended to be hidden from SPARK. The
problem
I have is that SPARK doesn't seem to get it:

   7    procedure C_Readlink_Boundary
                  ^
***        Semantic Error    :154: The subprogram or task body
C_Readlink_Boundary
           does not have an annotation.

The procedure doesn't touch any global variables. Any 'derives'
annotation added to the procedure is rejected by SPARK (as it would
need to
go on the procedure specification - which doesn't exist). I've used
the same
pattern on functions, not procedures, and SPARK has accepted it.

What have I done wrong here?