r235122 - in /trunk/gcc/ada: ChangeLog a-cuprqu...

[charlet@gcc.gnu.org]

Author: charlet
Date: Mon Apr 18 10:41:18 2016
New Revision: 235122

URL: https://gcc.gnu.org/viewcvs?rev=235122&root=gcc&view=rev
Log:
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.


Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/a-cuprqu.adb
    trunk/gcc/ada/a-nudira.adb
    trunk/gcc/ada/a-nudira.ads
    trunk/gcc/ada/a-nuflra.adb
    trunk/gcc/ada/a-nuflra.ads
    trunk/gcc/ada/exp_intr.adb
    trunk/gcc/ada/gnat1drv.adb
    trunk/gcc/ada/sem_prag.adb
    trunk/gcc/ada/sem_util.adb
    trunk/gcc/ada/sem_util.ads
    trunk/gcc/ada/spark_xrefs.ads