diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 33ff75bf2a6c..ed00e5450cf1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-07-31  Piotr Trojanek  <trojanek@adacore.com>
+
+	* ali.adb (Known_ALI_Lines): Remove 'F' as a prefix for lines
+	related to the FORMAL analysis done by GNATprove.
+
 2018-07-31  Javier Miranda  <miranda@adacore.com>
 
 	* sem.ads (Inside_Preanalysis_Without_Freezing): New global
diff --git a/gcc/ada/ali.adb b/gcc/ada/ali.adb
index 1cb454cce1ef..48b5715c7865 100644
--- a/gcc/ada/ali.adb
+++ b/gcc/ada/ali.adb
@@ -39,7 +39,7 @@ package body ALI is
    --  line type markers in the ALI file. This is used in Scan_ALI to detect
    --  (or skip) invalid lines. The following letters are still available:
    --
-   --    B G H J K O Q Z
+   --    B F G H J K O Q Z
 
    Known_ALI_Lines : constant array (Character range 'A' .. 'Z') of Boolean :=
      ('V'    => True,   -- version
@@ -59,7 +59,6 @@ package body ALI is
       'Y'    => True,   -- limited_with
       'Z'    => True,   -- implicit with from instantiation
       'C'    => True,   -- SCO information
-      'F'    => True,   -- SPARK cross-reference information
       'T'    => True,   -- task stack information
       others => False);