Replace use of SPARK_Mode Off on callers of procedure Move by stronger
preconditions, as mandated by Ada RM A.4.3, so that calls to the
corresponding functions inside the procedure bodies are provably
correct.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/a-strfix.adb (Delete, Insert, Overwrite,
	Replace_Slice): Remove SPARK_Mode Off.
	* libgnat/a-strfix.ads (Insert, Overwrite, Replace_Slice):
	Strengthen precondition.