This patch enables the check which ensures that a subprogram renaming does not
declare a primitive operation of a tagged type in instantiations.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-16 Hristian Kirtchev
* sem_ch8.adb (Check_SPARK_Primitive_Operation): Enable the c
This patch implements the following SPARK rules from SPARK RM 6.1.1(3):
A subprogram_renaming_declaration shall not declare a primitive operation of
a tagged type.
-- Source --
-- renamings.ads
package Renamings with SPARK_Mode is
type T is tagged null record
