[Ada] Fix failing assertions on SPARK elaboration

[Ada] Fix failing assertions on SPARK elaboration

Checking of SPARK elaboration rules may lead to assertion failures on a
compiler built with assertions. Now fixed.

There is no impact on compilation.

2019-08-14  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_disp.adb (Check_Dispatching_Operation): Update assertion
	for the separate declarations created in GNATprove mode.
	* sem_disp.ads (Is_Overriding_Subprogram): Update comment.
	* sem_elab.adb (SPARK_Processor): Fix test for checking of
	overriding primitives.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@274448 138bc75d-0d04-0410-961f-82ee72b054a4