[Ada] Fix lemma in generic unit System.Arith_Double

gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Word_Commutation): Fix for
	instances with other values of Single_Size.

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 0a75f08..57d427b 100644 (file)
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -541,7 +541,8 @@ is
    procedure Lemma_Word_Commutation (X : Single_Uns)
    with
      Ghost,
-     Post => Big_2xx32 * Big (Double_Uns (X)) = Big (2**32 * Double_Uns (X));
+     Post => Big_2xx32 * Big (Double_Uns (X))
+       = Big (2**Single_Size * Double_Uns (X));
 
    -----------------------------
    -- Local lemma null bodies --