Minor SPARK problem concerning 'redundant' with clauses.

[xorquewasp@googlemail.com]

I have a package P1 that uses the value of a constant defined in P2.

SPARK requires me to --# inherit P2 and the only place the annotation
can appear is in the spec of P1. The Ada compiler, however, sees that
the constant is only referenced in the body and complains loudly that
the 'with' clause is redundant and might be moved into the body of P2.

Is there a sensible solution to stop the two systems treading on each
other like this? In most cases, I can hack around the problem with a
spurious 'use type' clause (as much as I dislike it).

I tried to use pragma Warnings (Off) to wrap the "redundant" with
clauses, but of course SPARK immediately rejected it:

***        Syntax Error      : No complete PRAGMA_REP can be followed
by
           reserved word "WITH" here.