ada: Accept Modifies contract as a pragma

Typically, the recently added Modifies contract for SPARK will appear as an
aspect, but we also allow it to appear as a pragma, just like we do for Global,
Depends and other SPARK contracts.

gcc/ada/ChangeLog:

	* par-ch13.adb (P_Modifies_Specification): Now public, so it can be
	reused when parsing a pragma.
	* par-ch2.adb (P_Pragma): Parse pragma Modifies with a custom syntax.
	* par-prag.adb (Prag): A ??? comment is now implemented.
	* par.adb (P_Modifies_Specification): Now public, so it can be reused.