ada: Simplify dramatically ghost code for proof of System.Arith_Double

Using Inline_For_Proof annotation on key expression functions makes
it possible to remove hundreds of lines of ghost code that were
previously needed to guide provers.

gcc/ada/

	* libgnat/s-aridou.adb (Big3, Is_Mult_Decomposition)
	(Is_Scaled_Mult_Decomposition): Add annotation for inlining.
	(Double_Divide, Scaled_Divide): Simplify and remove ghost code.
	(Prove_Multiplication): Add calls to lemmas to make proof go
	through.
	* libgnat/s-aridou.ads (Big, In_Double_Int_Range): Add annotation
	for inlining.

0 files changed, 0 insertions, 0 deletions