--- a/gcc/ada/lib-xref.ads	Fri Oct 27 22:46:09 2017 +0900
+++ b/gcc/ada/lib-xref.ads	Thu Oct 25 07:37:49 2018 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1998-2017, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-2018, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -26,9 +26,8 @@
 --  This package contains for collecting and outputting cross-reference
 --  information.
 
-with Einfo;           use Einfo;
-with Lib.Util;        use Lib.Util;
-with Put_SPARK_Xrefs;
+with Einfo;       use Einfo;
+with SPARK_Xrefs;
 
 package Lib.Xref is
 
@@ -633,6 +632,11 @@
       --  Return the closest enclosing subprogram or library-level package.
       --  This ensures that GNATprove can distinguish local variables from
       --  global variables.
+      --
+      --  ??? This routine should only be used for processing related to
+      --  cross-references, where it might return wrong result but must avoid
+      --  crashes on ill-formed source code. It is wrong to use it where exact
+      --  result is needed.
 
       procedure Generate_Dereference
         (N   : Node_Id;
@@ -640,26 +644,15 @@
       --  This procedure is called to record a dereference. N is the location
       --  of the dereference.
 
-      procedure Collect_SPARK_Xrefs
-        (Sdep_Table : Unit_Ref_Table;
-         Num_Sdep   : Nat);
-      --  Collect SPARK cross-reference information from library units (for
-      --  files and scopes) and from shared cross-references. Fill in the
-      --  tables in library package called SPARK_Xrefs.
-
-      procedure Output_SPARK_Xrefs is new Put_SPARK_Xrefs;
-      --  Output SPARK cross-reference information to the ALI files, based on
-      --  the information collected in the tables in library package called
-      --  SPARK_Xrefs, and using routines in Lib.Util.
-
       generic
-         with procedure Process (N : Node_Id) is <>;
-      procedure Traverse_Compilation_Unit
-        (CU           : Node_Id;
-         Inside_Stubs : Boolean);
-      --  Call Process on all declarations within compilation unit CU. If
-      --  Inside_Stubs is True, then the body of stubs is also traversed.
-      --  Generic declarations are ignored.
+         with procedure Process
+           (Index : Int;
+            Xref  : SPARK_Xrefs.SPARK_Xref_Record);
+      procedure Iterate_SPARK_Xrefs;
+      --  Call Process on cross-references relevant to the SPARK backend with
+      --  parameter Xref holding the relevant subset of the xref entry and
+      --  Index holding the position in the original tables with references
+      --  (if positive) or dereferences (if negative).
 
    end SPARK_Specific;