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
