[multiple changes]

[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