ada: Implement change to SPARK RM rule on state refinement

ada: Implement change to SPARK RM rule on state refinement

SPARK RM 7.1.4(4) does not mandate anymore that a package with abstract
states has a completing body, unless the package state is mentioned in
Part_Of specifications. Implement that change.

gcc/ada/

	* sem_prag.adb (Check_Part_Of_Abstract_State): Add verification
	related to use of Part_Of, so that constituents in private childs
	that refer to state in a sibling or parent unit force that unit to
	have a body.
	* sem_util.adb (Check_State_Refinements): Drop the requirement to
	have always a package body for state refinement, when the package
	state is mentioned in no Part_Of specification.
	* sem_ch3.adb (Analyze_Declarations): Refresh SPARK refs in comment.
	* sem_ch7.adb (Analyze_Package_Declaration): Likewise.