Index: doc/gnat_ugn/elaboration_order_handling_in_gnat.rst
===================================================================
--- doc/gnat_ugn/elaboration_order_handling_in_gnat.rst	(revision 253753)
+++ doc/gnat_ugn/elaboration_order_handling_in_gnat.rst	(working copy)
@@ -133,9 +133,44 @@
 =================
 
 The sequence by which the elaboration code of all units within a partition is
-executed is referred to as **elaboration order**. The elaboration order depends
-on the following factors:
+executed is referred to as **elaboration order**.
 
+Within a single unit, elaboration code is executed in sequential order.
+
+::
+
+   package body Client is
+      Result : ... := Server.Func;
+
+      procedure Proc is
+         package Inst is new Server.Gen;
+      begin
+         Inst.Eval (Result);
+      end Proc;
+   begin
+      Proc;
+   end Client;
+
+In the example above, the elaboration order within package body ``Client`` is
+as follows:
+
+1. The object declaration of ``Result`` is elaborated.
+
+   * Function ``Server.Func`` is invoked.
+
+2. The subprogram body of ``Proc`` is elaborated.
+
+3. Procedure ``Proc`` is invoked.
+
+   * Generic unit ``Server.Gen`` is instantiated as ``Inst``.
+
+   * Instance ``Inst`` is elaborated.
+
+   * Procedure ``Inst.Eval`` is invoked.
+
+The elaboration order of all units within a partition depends on the following
+factors:
+
 * |withed| units
 
 * purity of units
@@ -571,7 +606,7 @@
   a partition is elaboration code. GNAT performs very few diagnostics and
   generates run-time checks to verify the elaboration order of a program. This
   behavior is identical to that specified by the Ada Reference Manual. The
-  dynamic model is enabled with compilation switch :switch:`-gnatE`.
+  dynamic model is enabled with compiler switch :switch:`-gnatE`.
 
 .. index:: Static elaboration model
 
@@ -860,7 +895,7 @@
 The SPARK model is identical to the static model in its handling of internal
 targets. The SPARK model, however, requires explicit ``Elaborate`` or
 ``Elaborate_All`` pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch :switch:`-gnatd.v` is in effect.
 
 ::
 
@@ -987,7 +1022,7 @@
 * *Switch to more permissive elaboration model*
 
   If the compilation was performed using the static model, enable the dynamic
-  model with compilation switch :switch:`-gnatE`. GNAT will no longer generate
+  model with compiler switch :switch:`-gnatE`. GNAT will no longer generate
   implicit ``Elaborate`` and ``Elaborate_All`` pragmas, resulting in a behavior
   identical to that specified by the Ada Reference Manual. The binder will
   generate an executable program that may or may not raise ``Program_Error``,
@@ -1504,6 +1539,17 @@
   When this switch is in effect, GNAT will ignore ``'Access`` of an entry,
   operator, or subprogram when the static model is in effect.
 
+.. index:: -gnatd.v  (gnat)
+
+:switch:`-gnatd.v`
+  Enforce SPARK elaboration rules in SPARK code
+
+  When this switch is in effect, GNAT will enforce the SPARK rules of
+  elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+  result, constructs which violate the SPARK elaboration rules are no longer
+  accepted, even if GNAT is able to statically ensure that these constructs
+  will not lead to ABE problems.
+
 .. index:: -gnatd.y  (gnat)
 
 :switch:`-gnatd.y`
@@ -1558,7 +1604,7 @@
   - *SPARK model*
 
     GNAT will indicate how an elaboration requirement is met by the context of
-    a unit.
+    a unit. This diagnostic requires compiler switch :switch:`-gnatd.v`.
 
     ::
 
@@ -1612,8 +1658,8 @@
 elaboration order, then apart from possible cases involing dispatching calls
 and access-to-subprogram types, the program is free of elaboration errors.
 If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch :switch:`-gnatel` and
-consider the messages about missing or implicitly created ``Elaborate`` and
+then the programmer should use compiler switch :switch:`-gnatel` and consider
+the messages about missing or implicitly created ``Elaborate`` and
 ``Elaborate_All`` pragmas.
 
 If the binder reports an elaboration circularity, the programmer has several
Index: sem_elab.adb
===================================================================
--- sem_elab.adb	(revision 253756)
+++ sem_elab.adb	(working copy)
@@ -361,6 +361,13 @@
    --           entries, operators, and subprograms. As a result, the scenarios
    --           are not recorder or processed.
    --
+   --  -gnatd.v enforce SPARK elaboration rules in SPARK code
+   --
+   --           The ABE mechanism applies some of the SPARK elaboration rules
+   --           defined in the SPARK reference manual, chapter 7.7. Note that
+   --           certain rules are always enforced, regardless of whether the
+   --           switch is active.
+   --
    --  -gnatd.y disable implicit pragma Elaborate_All on task bodies
    --
    --           The ABE mechanism does not generate implicit Elaborate_All when
@@ -6891,16 +6898,18 @@
       elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
+      --  elaboration rules in SPARK code) is in effect.
 
-      elsif SPARK_Rules_On then
+      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
          Process_Call_SPARK
            (Call         => Call,
             Call_Attrs   => Call_Attrs,
             Target_Id    => Target_Id,
             Target_Attrs => Target_Attrs);
 
-      --  Otherwise the Ada rules are in effect
+      --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
+      --  violate the SPARK rules.
 
       else
          Process_Call_Ada
@@ -7459,9 +7468,10 @@
       elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
+      --  elaboration rules in SPARK code) is in effect.
 
-      elsif SPARK_Rules_On then
+      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
          Process_Instantiation_SPARK
            (Exp_Inst   => Exp_Inst,
             Inst       => Inst,
@@ -7469,7 +7479,8 @@
             Gen_Id     => Gen_Id,
             Gen_Attrs  => Gen_Attrs);
 
-      --  Otherwise the Ada rules are in effect
+      --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
+      --  violate the SPARK rules.
 
       else
          Process_Instantiation_Ada
@@ -7869,7 +7880,10 @@
             In_SPARK => SPARK_Rules_On);
       end if;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are in effect. These rules are applied regardless of
+      --  whether -gnatd.v (enforce SPARK elaboration rules in SPARK code) is
+      --  in effect because the static model cannot ensure safe assignment of
+      --  variables.
 
       if SPARK_Rules_On then
          Process_Variable_Assignment_SPARK
Index: debug.adb
===================================================================
--- debug.adb	(revision 253753)
+++ debug.adb	(working copy)
@@ -112,7 +112,7 @@
    --  d.s  Strict secondary stack management
    --  d.t  Disable static allocation of library level dispatch tables
    --  d.u  Enable Modify_Tree_For_C (update tree for c)
-   --  d.v
+   --  d.v  Enforce SPARK elaboration rules in SPARK code
    --  d.w  Do not check for infinite loops
    --  d.x  No exception handlers
    --  d.y  Disable implicit pragma Elaborate_All on task bodies
@@ -600,6 +600,13 @@
    --  d.u  Sets Modify_Tree_For_C mode in which tree is modified to make it
    --       easier to generate code using a C compiler.
 
+   --  d.v  This flag enforces the elaboration rules defined in the SPARK
+   --       Reference Manual, chapter 7.7, to all SPARK code within a unit. As
+   --       a result, constructs which violate the rules in chapter 7.7 are no
+   --       longer accepted, even if the implementation is able to statically
+   --       ensure that accepting these constructs does not introduce the
+   --       possibility of failing an elaboration check.
+
    --  d.w  This flag turns off the scanning of loops to detect possible
    --       infinite loops.
 
Index: gnat_ugn.texi
===================================================================
--- gnat_ugn.texi	(revision 253753)
+++ gnat_ugn.texi	(working copy)
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT User's Guide for Native Platforms , Oct 09, 2017
+GNAT User's Guide for Native Platforms , Oct 14, 2017
 
 AdaCore
 
@@ -27187,13 +27187,67 @@
 
 
 The sequence by which the elaboration code of all units within a partition is
-executed is referred to as @strong{elaboration order}. The elaboration order depends
-on the following factors:
+executed is referred to as @strong{elaboration order}.
 
+Within a single unit, elaboration code is executed in sequential order.
 
+@example
+package body Client is
+   Result : ... := Server.Func;
+
+   procedure Proc is
+      package Inst is new Server.Gen;
+   begin
+      Inst.Eval (Result);
+   end Proc;
+begin
+   Proc;
+end Client;
+@end example
+
+In the example above, the elaboration order within package body @code{Client} is
+as follows:
+
+
+@enumerate 
+
+@item 
+The object declaration of @code{Result} is elaborated.
+
+
 @itemize *
 
 @item 
+Function @code{Server.Func} is invoked.
+@end itemize
+
+@item 
+The subprogram body of @code{Proc} is elaborated.
+
+@item 
+Procedure @code{Proc} is invoked.
+
+
+@itemize *
+
+@item 
+Generic unit @code{Server.Gen} is instantiated as @code{Inst}.
+
+@item 
+Instance @code{Inst} is elaborated.
+
+@item 
+Procedure @code{Inst.Eval} is invoked.
+@end itemize
+@end enumerate
+
+The elaboration order of all units within a partition depends on the following
+factors:
+
+
+@itemize *
+
+@item 
 @emph{with}ed units
 
 @item 
@@ -27689,7 +27743,7 @@
 a partition is elaboration code. GNAT performs very few diagnostics and
 generates run-time checks to verify the elaboration order of a program. This
 behavior is identical to that specified by the Ada Reference Manual. The
-dynamic model is enabled with compilation switch @code{-gnatE}.
+dynamic model is enabled with compiler switch @code{-gnatE}.
 @end itemize
 
 @geindex Static elaboration model
@@ -28001,7 +28055,7 @@
 The SPARK model is identical to the static model in its handling of internal
 targets. The SPARK model, however, requires explicit @code{Elaborate} or
 @code{Elaborate_All} pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch @code{-gnatd.v} is in effect.
 
 @example
 1. with Server;
@@ -28146,7 +28200,7 @@
 @emph{Switch to more permissive elaboration model}
 
 If the compilation was performed using the static model, enable the dynamic
-model with compilation switch @code{-gnatE}. GNAT will no longer generate
+model with compiler switch @code{-gnatE}. GNAT will no longer generate
 implicit @code{Elaborate} and @code{Elaborate_All} pragmas, resulting in a behavior
 identical to that specified by the Ada Reference Manual. The binder will
 generate an executable program that may or may not raise @code{Program_Error},
@@ -28711,6 +28765,22 @@
 operator, or subprogram when the static model is in effect.
 @end table
 
+@geindex -gnatd.v (gnat)
+
+
+@table @asis
+
+@item @code{-gnatd.v}
+
+Enforce SPARK elaboration rules in SPARK code
+
+When this switch is in effect, GNAT will enforce the SPARK rules of
+elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+result, constructs which violate the SPARK elaboration rules are no longer
+accepted, even if GNAT is able to statically ensure that these constructs
+will not lead to ABE problems.
+@end table
+
 @geindex -gnatd.y (gnat)
 
 
@@ -28785,7 +28855,7 @@
 @emph{SPARK model}
 
 GNAT will indicate how an elaboration requirement is met by the context of
-a unit.
+a unit. This diagnostic requires compiler switch @code{-gnatd.v}.
 
 @example
 1. with Server; pragma Elaborate_All (Server);
@@ -28846,8 +28916,8 @@
 elaboration order, then apart from possible cases involing dispatching calls
 and access-to-subprogram types, the program is free of elaboration errors.
 If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch @code{-gnatel} and
-consider the messages about missing or implicitly created @code{Elaborate} and
+then the programmer should use compiler switch @code{-gnatel} and consider
+the messages about missing or implicitly created @code{Elaborate} and
 @code{Elaborate_All} pragmas.
 
 If the binder reports an elaboration circularity, the programmer has several
