[Ada] Add missing Global contract to Ada.Containers.Functional_Vectors

2020-06-05  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* libgnat/a-cofuve.ads (First): Add Global contract.

diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index 7a48a5a319d9591598b46e48974f15a6fd3ba1b0..cfccf1d157f992512c75fd669333813bbb0434bd 100644 (file)
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -92,7 +92,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
            Length (Container));
    pragma Annotate (GNATprove, Inline_For_Proof, Last);
 
-   function First return Extended_Index is (Index_Type'First);
+   function First return Extended_Index is (Index_Type'First) with
+     Global => null;
    --  First index of a sequence
 
    ------------------------