Unqualified enum literal from different package undetected

[senier]

When using an unqualified enumeration literal in the condition of a refinement and the respective enumeration is specified in a separate package, the refinement is accepted as correct, but the generated SPARK code does not compile. Example:

package Numbers is
   type Protocol is (PROTO_OUTER) with Size => 8;
end Numbers;

with Numbers;
package Proto is
   type Packet is
      message
         Protocol : Numbers::Protocol
            then Data
               with Size => 128;
         Data  : Opaque;
      end message;
end Proto;

package Inner is
   type Value is mod 2**8;
   type Packet is
      message
         Data : Value;
      end message;
end Inner;

with Proto;
with Inner;
package In_Proto is
   for Proto::Packet use (Data => Inner::Packet)
      if Protocol = PROTO_OUTER;
end In_Proto;

$ rflx generate -d build in_proto.rflx 
Parsing in_proto.rflx
Parsing proto.rflx
Parsing numbers.rflx
Parsing inner.rflx
Processing Inner
Processing Numbers
Processing Proto
Processing In_Proto
Creating build/rflx-inner.ads
Creating build/rflx-inner-generic_packet.ads
Creating build/rflx-inner-generic_packet.adb
Creating build/rflx-inner-packet.ads
Creating build/rflx-numbers.ads
Creating build/rflx-proto.ads
Creating build/rflx-proto-generic_packet.ads
Creating build/rflx-proto-generic_packet.adb
Creating build/rflx-proto-packet.ads
Creating build/rflx-in_proto.ads
Creating build/rflx-in_proto-generic_contains.ads
Creating build/rflx-in_proto-generic_contains.adb
Creating build/rflx-in_proto-contains.ads
Creating build/rflx-rflx_arithmetic.ads
Creating build/rflx-rflx_builtin_types-conversions.ads
Creating build/rflx-rflx_builtin_types.ads
Creating build/rflx-rflx_generic_types.ads
Creating build/rflx-rflx_message_sequence.ads
Creating build/rflx-rflx_scalar_sequence.ads
Creating build/rflx-rflx_types.ads
Creating build/rflx-rflx_arithmetic.adb
Creating build/rflx-rflx_generic_types.adb
Creating build/rflx-rflx_message_sequence.adb
Creating build/rflx-rflx_scalar_sequence.adb
Creating build/rflx.ads
$ gprbuild -P build
Compile
   [Ada]          rflx-numbers.ads
   [Ada]          rflx-proto-packet.ads
   [Ada]          rflx-rflx_types.ads
   [Ada]          rflx-rflx_builtin_types.ads
   [Ada]          rflx-rflx_generic_types.adb
   [Ada]          rflx-in_proto-generic_contains.adb
rflx-in_proto-generic_contains.ads:33:50: "PROTO_OUTER" is not visible
rflx-in_proto-generic_contains.ads:33:50: non-visible declaration at rflx-numbers.ads:18
gprbuild: *** compilation phase failed

Importing the Numbers package and prefixing the literal with Numbers:: yields

rflx-in_proto-generic_contains.ads:33:50: "Numbers" is not visible
rflx-in_proto-generic_contains.ads:33:50: non-visible declaration at rflx-numbers.ads:12

The unprefixed literal should be reject in the spec and the SPARK package containing the definition should be withed in the generated code.