[gcc(refs/users/marxin/heads/slp-function-v2)] [Ada] Add missing Global contract to Ada.Containers.Functional_Vectors

[Martin Liska]

https://gcc.gnu.org/g:a8aecf319aaa77429584ac8c18f556c2577616b9

commit a8aecf319aaa77429584ac8c18f556c2577616b9
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Fri Jan 31 21:13:31 2020 +0100

    [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:
---
 gcc/ada/libgnat/a-cofuve.ads | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index 7a48a5a319d..cfccf1d157f 100644
--- 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
 
    ------------------------