diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3289f77df69..974ff3fb7e7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2011-08-04  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch3.adb (Analyze_Object_Declaration): remove obsolete addition of
+	reference for ALFA mode.
+	* lib-xref-alfa.adb, lib-xref.ads (Traverse_Compilation_Unit): make
+	procedure public so as to use it from formal verification back-end.
+
 2011-08-04  Jerome Lambourg  <lambourg@adacore.com>
 
 	* g-comlin.adb (For_Each_Simple_Switch.Is_In_Config): Remove the
diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb
index b650d389809..701de0b8624 100644
--- a/gcc/ada/lib-xref-alfa.adb
+++ b/gcc/ada/lib-xref-alfa.adb
@@ -164,9 +164,6 @@ package body ALFA is
    function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
    --  Hash function for hash table
 
-   procedure Traverse_Compilation_Unit
-     (CU      : Node_Id;
-      Process : Node_Processing);
    procedure Traverse_Declarations_Or_Statements
      (L       : List_Id;
       Process : Node_Processing);
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 3d6252efb31..5ddc273cf52 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -593,6 +593,10 @@ package Lib.Xref is
 
       type Node_Processing is access procedure (N : Node_Id);
 
+      procedure Traverse_Compilation_Unit
+        (CU      : Node_Id;
+         Process : Node_Processing);
+
       procedure Traverse_All_Compilation_Units (Process : Node_Processing);
       --  Call Process on all declarations through all compilation units
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 283f8405bce..d43fd271a9a 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3740,13 +3740,6 @@ package body Sem_Ch3 is
       if Has_Aspects (N) then
          Analyze_Aspect_Specifications (N, Id);
       end if;
-
-      --  Generate 'I' xref for object initialization at definition, only used
-      --  for the local xref section used in ALFA mode.
-
-      if ALFA_Mode and then Present (Expression (Original_Node (N))) then
-         Generate_Reference (Id, Id, 'I');
-      end if;
    end Analyze_Object_Declaration;
 
    ---------------------------