[Ada] Clean ups in SPARK mode

Index: exp_spark.adb
===================================================================
--- exp_spark.adb	(revision 203568)
+++ exp_spark.adb	(working copy)
@@ -25,7 +25,6 @@ 
 
 with Atree;    use Atree;
 with Einfo;    use Einfo;
-with Exp_Ch4;  use Exp_Ch4;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
 with Sem_Aux;  use Sem_Aux;
@@ -80,12 +79,6 @@ 
               N_Identifier    =>
             Expand_Potential_Renaming (N);
 
-         --  A NOT IN B gets transformed to NOT (A IN B). This is the same
-         --  expansion used in the normal case, so shared the code.
-
-         when N_Not_In =>
-            Expand_N_Not_In (N);
-
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
 
Index: exp_spark.ads
===================================================================
--- exp_spark.ads	(revision 203568)
+++ exp_spark.ads	(working copy)
@@ -30,54 +30,6 @@ 
 
 --  Expand_SPARK is called directly by Expander.Expand.
 
---  SPARK expansion has three main objectives:
-
---    1. Perform limited expansion to explicit some Ada rules and constructs
---       (translate 'Old and 'Result, replace renamings by renamed, insert
---        conversions, expand actuals in calls to introduce temporaries, expand
---        generics instantiations)
-
---    2. Facilitate treatment for the formal verification back-end (fully
---       qualify names, expand set membership, compute data dependences)
-
---    3. Avoid the introduction of low-level code that is difficult to analyze
---       formally, as typically done in the full expansion for high-level
---       constructs (tasking, dispatching)
-
---  To fulfill objective 1, Expand_SPARK selectively expands some constructs.
-
---  To fulfill objective 2, the tree after SPARK expansion should be fully
---  analyzed semantically. In particular, all expression must have their proper
---  type, and semantic links should be set between tree nodes (partial to full
---  view, etc.) Some kinds of nodes should be either absent, or can be ignored
---  by the formal verification backend:
-
---      N_Object_Renaming_Declaration: can be ignored safely
---      N_Expression_Function:         absent (rewitten)
---      N_Expression_With_Actions:     absent (not generated)
-
---  SPARK cross-references are generated from the regular cross-references
---  (used for browsing and code understanding) and additional references
---  collected during semantic analysis, in particular on all
---  dereferences. These SPARK cross-references are output in a separate section
---  of ALI files, as described in spark_xrefs.adb. They are the basis for the
---  computation of data dependences in the formal verification backend. This
---  implies that all cross-references should be generated in this mode, even
---  those that would not make sense from a user point-of-view, and that
---  cross-references that do not lead to data dependences for subprograms can
---  be safely ignored.
-
---  To support the formal verification of units parameterized by data, the
---  value of deferred constants should not be considered as a compile-time
---  constant at program locations where the full view is not visible.
-
---  To fulfill objective 3, Expand_SPARK does not expand features that are not
---  formally analyzed (tasking), or for which formal analysis relies on the
---  source level representation (dispatching, aspects, pragmas). However, these
---  should be semantically analyzed, which sometimes requires the insertion of
---  semantic pre-analysis, for example for subprogram contracts and pragma
---  check/assert.
-
 with Types; use Types;
 
 package Exp_SPARK is
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 203568)
+++ sinfo.ads	(working copy)
@@ -508,6 +508,48 @@ 
    --      simply ignore these nodes, since they are not relevant to the task
    --      of back annotating representation information.
 
+   ----------------
+   -- SPARK Mode --
+   ----------------
+
+   --  When a file is compiled in SPARK mode (-gnatd.F), a very light expansion
+   --  is performed and the analysis must generate a tree in a form that meets
+   --  additional requirements.
+
+   --  The SPARK expansion does two transformations of the tree, that cannot be
+   --  postponed after the frontend semantic analysis:
+
+   --    1. Replace renamings by renamed (object/subprogram). This requires
+   --       introducing temporaries at the point of the renaming, which must be
+   --       properly analyzed.
+
+   --    2. Fully qualify entity names. This is needed to generate suitable
+   --       local effects/call-graphs in ALI files, with the completely
+   --       qualified names (in particular the suffix to distinguish homonyms).
+
+   --  The tree after SPARK expansion should be fully analyzed semantically,
+   --  which sometimes requires the insertion of semantic pre-analysis, for
+   --  example for subprogram contracts and pragma check/assert. In particular,
+   --  all expression must have their proper type, and semantic links should be
+   --  set between tree nodes (partial to full view, etc.) Some kinds of nodes
+   --  should be either absent, or can be ignored by the formal verification
+   --  backend:
+
+   --      N_Object_Renaming_Declaration: can be ignored safely
+   --      N_Expression_Function:         absent (rewitten)
+   --      N_Expression_With_Actions:     absent (not generated)
+
+   --  SPARK cross-references are generated from the regular cross-references
+   --  (used for browsing and code understanding) and additional references
+   --  collected during semantic analysis, in particular on all dereferences.
+   --  These SPARK cross-references are output in a separate section of ALI
+   --  files, as described in spark_xrefs.adb. They are the basis for the
+   --  computation of data dependences in the formal verification backend.
+   --  This implies that all cross-references should be generated in this mode,
+   --  even those that would not make sense from a user point-of-view, and that
+   --  cross-references that do not lead to data dependences for subprograms
+   --  can be safely ignored.
+
    ------------------------
    -- Common Flag Fields --
    ------------------------