[Ada] Remove a SPARK rule about implicit Global
authorPiotr Trojanek <trojanek@adacore.com>
Mon, 1 Jul 2019 13:37:06 +0000 (13:37 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 1 Jul 2019 13:37:06 +0000 (13:37 +0000)
commit9d8aaa4e00958418c01a4aee5a08261108eaf997
tree8f0b9daed4376b3da593b9c85bb8cdf7c9ea3340
parent397348b919d12c643071ebf0ef79b2c663682523
[Ada] Remove a SPARK rule about implicit Global

A rule about implicit Global contract for functions whose names overload
an abstract state was never implemented (and no user complained about
this). It is now removed, so references to other rules need to be
renumbered.

2019-07-01  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

* einfo.adb, sem_ch7.adb, sem_prag.adb, sem_util.adb: Update
references to the SPARK RM after the removal of Rule 7.1.4(5).

From-SVN: r272875
gcc/ada/ChangeLog
gcc/ada/einfo.adb
gcc/ada/sem_ch7.adb
gcc/ada/sem_prag.adb
gcc/ada/sem_util.adb