| -- { dg-do compile } | |
| -- { dg-options "-gnatd.F" } | |
| procedure Generic_Actuals with SPARK_Mode is | |
| generic | |
| X : Integer; | |
| Y : Integer := 0; | |
| package Q with Initializes => (XX => X, YY => Y) is | |
| -- Both X and Y actuals can appear in the Initializes contract, | |
| -- i.e. the default expression of Y should not matter. | |
| XX : Integer := X; | |
| YY : Integer := Y; | |
| end Q; | |
| package Inst is new Q (X => 0); | |
| begin | |
| null; | |
| end Generic_Actuals; |