SPARK: Problem with using constants in a post annotation

[George <geo.paok@gmail.com>]

Hello,

I'm trying to use inside a post annotation two constants that are
declared in the package body. But, I can't do it, because the two
constants are not recognised at the point where they are used in the
annotation. Does anyone have an idea of how to overcome this problem?
Is it possible to overcome this by using only annotations without
changing the code?
The package specification and body, as well as the error messages are
shown below:

-- File P2.ads
--# inherit P1;
package P2
is
   procedure Control;
   --# global in out P1.Val;
   --# derives P1.Val from P1.Val;
   --# post (P1.Val <= [COLOR="Red"][B]C1[/B][/COLOR] -> P1.Val = 0)
and
   --#      (P1.Val >= [COLOR="Red"][B]C2[/B][/COLOR] -> P1.Val = 1);

end P2;


-- File P2.adb
with P1;
package body P2 is

   C1: constant P1.Type := 10;
   C2: constant P1.Type := 20;

   procedure Proc
   is
      V1: P1.Type;
   begin
      V1 := P1.Val;
      if V1 <= C1 then
         P1.Val := 0;
      elsif V1 >= C2 then
         P1.Val := 1;
      end if;
   end Proc;

end P2;


OUTPUT
13:30   Semantic Error   1 - The identifier C1 is either undeclared or
not visible at this point.
14:30   Semantic Error   1 - The identifier C2 is either undeclared or
not visible at this point.