Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 213566)
+++ sem_ch3.adb	(working copy)
@@ -15046,7 +15046,7 @@
       end if;
 
       --  Only composite types other than array types are allowed to have
-      --  discriminants. In SPARK, no types are allowed to have discriminants.
+      --  discriminants.
 
       if Present (Discriminant_Specifications (N)) then
          if (Is_Elementary_Type (Parent_Type)
@@ -15057,8 +15057,22 @@
               ("elementary or array type cannot have discriminants",
                Defining_Identifier (First (Discriminant_Specifications (N))));
             Set_Has_Discriminants (T, False);
+
+         --  The type is allowed to have discriminants
+
          else
             Check_SPARK_05_Restriction ("discriminant type is not allowed", N);
+
+            --  The following check is only relevant when SPARK_Mode is on as
+            --  it is not a standard Ada legality rule. A derived type cannot
+            --  have discriminants if the parent type is discriminated.
+
+            if SPARK_Mode = On and then Has_Discriminants (Parent_Type) then
+               SPARK_Msg_N
+                 ("discriminants not allowed if parent type is discriminated",
+                  Defining_Identifier
+                    (First (Discriminant_Specifications (N))));
+            end if;
          end if;
       end if;
 
@@ -18024,24 +18038,44 @@
             end if;
          end if;
 
-         if Is_Access_Type (Discr_Type) then
+         --  The following checks are only relevant when SPARK_Mode is on as
+         --  they are not standard Ada legality rules.
 
-            --  Ada 2005 (AI-230): Access discriminant allowed in non-limited
-            --  record types
+         if SPARK_Mode = On then
+            if Is_Access_Type (Discr_Type) then
+               SPARK_Msg_N
+                 ("discriminant cannot have an access type",
+                  Discriminant_Type (Discr));
 
-            if Ada_Version < Ada_2005 then
-               Check_Access_Discriminant_Requires_Limited
-                 (Discr, Discriminant_Type (Discr));
+            elsif not Is_Discrete_Type (Discr_Type) then
+               SPARK_Msg_N
+                 ("discriminant must have a discrete type",
+                  Discriminant_Type (Discr));
             end if;
 
-            if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then
+         --  Normal Ada rules
+
+         else
+            if Is_Access_Type (Discr_Type) then
+
+               --  Ada 2005 (AI-230): Access discriminant allowed in non-
+               --  limited record types
+
+               if Ada_Version < Ada_2005 then
+                  Check_Access_Discriminant_Requires_Limited
+                    (Discr, Discriminant_Type (Discr));
+               end if;
+
+               if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then
+                  Error_Msg_N
+                    ("(Ada 83) access discriminant not allowed", Discr);
+               end if;
+
+            elsif not Is_Discrete_Type (Discr_Type) then
                Error_Msg_N
-                 ("(Ada 83) access discriminant not allowed", Discr);
+                 ("discriminants must have a discrete or access type",
+                  Discriminant_Type (Discr));
             end if;
-
-         elsif not Is_Discrete_Type (Discr_Type) then
-            Error_Msg_N ("discriminants must have a discrete or access type",
-              Discriminant_Type (Discr));
          end if;
 
          Set_Etype (Defining_Identifier (Discr), Discr_Type);
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 213570)
+++ sem_ch7.adb	(working copy)
@@ -439,7 +439,7 @@
 
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if not Inside_A_Generic and then Present (SPARK_Pragma (Body_Id)) then
+      if Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Aux_Pragma (Spec_Id)) then
             if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
                  and then
Index: a-cfhase.ads
===================================================================
--- a-cfhase.ads	(revision 213536)
+++ a-cfhase.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -70,6 +70,7 @@
 package Ada.Containers.Formal_Hashed_Sets is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -329,8 +330,8 @@
    --  scanned yet.
 
 private
-
    pragma Inline (Next);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is
       record
@@ -343,7 +344,7 @@
      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is
-      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
 
    use HT_Types;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 213571)
+++ sem_prag.adb	(working copy)
@@ -19243,13 +19243,6 @@
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
-
-            --  Do not analyze the pragma when it appears inside a generic
-            --  because the semantic information of the related context is
-            --  scarce.
-
-            elsif Inside_A_Generic then
-               return;
             end if;
 
             GNAT_Pragma;
Index: a-cforma.ads
===================================================================
--- a-cforma.ads	(revision 213536)
+++ a-cforma.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -69,6 +69,7 @@
 package Ada.Containers.Formal_Ordered_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
      Global => null;
@@ -265,10 +266,11 @@
    function Overlap (Left, Right : Map) return Boolean with
      Global => null;
    --  Overlap returns True if the containers have common keys
+
 private
-
    pragma Inline (Next);
    pragma Inline (Previous);
+   pragma SPARK_Mode (Off);
 
    subtype Node_Access is Count_Type;
 
@@ -288,7 +290,7 @@
      new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
 
    type Map (Capacity : Count_Type) is
-      new Tree_Types.Tree_Type (Capacity) with null record;
+     new Tree_Types.Tree_Type (Capacity) with null record;
 
    type Cursor is record
       Node : Node_Access;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 213571)
+++ sem_ch6.adb	(working copy)
@@ -3741,10 +3741,7 @@
 
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
-      if not Inside_A_Generic
-        and then Present (Spec_Id)
-        and then Present (SPARK_Pragma (Body_Id))
-      then
+      if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Pragma (Spec_Id)) then
             if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
                  and then
Index: a-cfhama.ads
===================================================================
--- a-cfhama.ads	(revision 213536)
+++ a-cfhama.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -68,6 +68,7 @@
 package Ada.Containers.Formal_Hashed_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
@@ -276,6 +277,7 @@
    pragma Inline (Has_Element);
    pragma Inline (Equivalent_Keys);
    pragma Inline (Next);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Key         : Key_Type;
@@ -285,11 +287,10 @@
    end record;
 
    package HT_Types is new
-     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
-       (Node_Type);
+     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is
-      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+     new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
 
    use HT_Types;
 
Index: a-cforse.ads
===================================================================
--- a-cforse.ads	(revision 213536)
+++ a-cforse.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -67,6 +67,7 @@
 package Ada.Containers.Formal_Ordered_Sets is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
+   pragma SPARK_Mode (On);
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
    with
@@ -347,9 +348,9 @@
    --  scanned yet.
 
 private
-
    pragma Inline (Next);
    pragma Inline (Previous);
+   pragma SPARK_Mode (Off);
 
    type Node_Type is record
       Has_Element : Boolean := False;
