diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2021-11-22 19:01:33 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:24 +0000 |
| commit | eca89ac6e73026a8606e05e6f0486f963c02c4bc (patch) | |
| tree | 7f13f9a33da568abdb00528fd77e8c7bbf85d0b1 /gcc/ada/sem_ch12.adb | |
| parent | 5ae5ba7ab10f9cc4d897f0553c472f33875453e0 (diff) | |
| download | gcc-eca89ac6e73026a8606e05e6f0486f963c02c4bc.zip gcc-eca89ac6e73026a8606e05e6f0486f963c02c4bc.tar.gz gcc-eca89ac6e73026a8606e05e6f0486f963c02c4bc.tar.bz2 | |
[Ada] Enable expansion of dispatching equality for GNATprove
gcc/ada/
* exp_ch13.ads (Expand_N_Freeze_Entity): Add note about a SPARK
twin.
* exp_ch3.ads (Freeze_Type): Likewise.
* exp_spark.adb (Expand_SPARK_N_Freeze_Entity): Mimic what is
done in Freeze_Entity.
(SPARK_Freeze_Type): Mimic what is done in Freeze_Type; add call
to Make_Predefined_Primitive_Eq_Spec.
Diffstat (limited to 'gcc/ada/sem_ch12.adb')
0 files changed, 0 insertions, 0 deletions