diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-04-18 12:41:18 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-04-18 12:41:18 +0200 |
| commit | 1f55088db5038881cc4836ba600edb1bb8fe0141 (patch) | |
| tree | 1a5dcd40078c74bc1cd52b4cdd52caafe65fb4e6 /gcc/ada/spark_xrefs.ads | |
| parent | 142870f570d036ec06127bad47679743e68010f7 (diff) | |
| download | gcc-1f55088db5038881cc4836ba600edb1bb8fe0141.zip gcc-1f55088db5038881cc4836ba600edb1bb8fe0141.tar.gz gcc-1f55088db5038881cc4836ba600edb1bb8fe0141.tar.bz2 | |
[multiple changes]
2016-04-18 Yannick Moy <moy@adacore.com>
* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used
outside of GNATprove, hence it should not be removed.
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Refinement_Clause):
The refinement of an external abstract state can now mention
non-external constituents.
(Check_External_Property): Update all SPARK RM references.
2016-04-18 Bob Duff <duff@adacore.com>
* exp_intr.adb: Remove some duplicated code.
2016-04-18 Yannick Moy <moy@adacore.com>
* a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark
package spec and body out of SPARK.
2016-04-18 Johannes Kanig <kanig@adacore.com>
* spark_xrefs.ads: Minor comment update.
2016-04-18 Johannes Kanig <kanig@adacore.com>
* gnat1drv.adb (Gnat1drv): Force loading of System
unit for SPARK.
2016-04-18 Bob Duff <duff@adacore.com>
* a-cuprqu.adb: Correction to previous change. If a new node
is inserted at the front of the queue (because it is higher
priority than the previous front node), we need to update
Header.Next_Unequal -- not just in the case where the queue was
previously empty.
From-SVN: r235122
Diffstat (limited to 'gcc/ada/spark_xrefs.ads')
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index eb95f73..f02234f 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -200,7 +200,7 @@ package SPARK_Xrefs is -- not relate to Generated Globals. -- The processing (reading and writing) of this section happens in - -- package Flow_Computed_Globals (from the SPARK 2014 sources), for + -- package Flow_Generated_Globals (from the SPARK 2014 sources), for -- further information please refer there. ---------------- |