sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Adapt checking for optional...

sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Adapt checking for optional refinement of abstract state with partial visible...

2016-10-12  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Analyze_Refined_Depends_In_Decl_Part): Adapt checking
	for optional refinement of abstract state with partial
	visible refinement.
	(Analyze_Refined_Global_In_Decl_Part): Adapt checking for optional
	refinement of abstract state with partial visible refinement. Implement
	new rules in SPARK RM 7.2.4 related to optional refinement.
	Also fix the missing detection of missing items.

From-SVN: r241050