[gcc(refs/users/aoliva/heads/testme)] [Ada] Revert workaround for expansion of Enum_Rep in GNATprove mode

[Alexandre Oliva]

https://gcc.gnu.org/g:8ecc34842c6884a508aaf56328ee76576c348cf7

commit 8ecc34842c6884a508aaf56328ee76576c348cf7
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Thu Mar 5 11:57:50 2020 +0100

    [Ada] Revert workaround for expansion of Enum_Rep in GNATprove mode
    
    2020-06-10  Piotr Trojanek  <trojanek@adacore.com>
    
    gcc/ada/
    
            * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove
            expansion of First and Last attributes.

Diff:
---
 gcc/ada/exp_spark.adb | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index cab48f49b5c..0e6c745270a 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -52,14 +52,13 @@ package body Exp_SPARK is
    -----------------------
 
    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-   --  Replace occurrences of System'To_Address by calls to
-   --  System.Storage_Elements.To_Address
+   --  Perform attribute-reference-specific expansion
 
    procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
    --  Build the DIC procedure of a type when needed, if not already done
 
    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
-   --  Perform loop statement-specific expansion
+   --  Perform loop-statement-specific expansion
 
    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
    --  Perform object-declaration-specific expansion
@@ -266,12 +265,6 @@ package body Exp_SPARK is
             Analyze_And_Resolve (N, Standard_Boolean);
          end if;
 
-      --  For attributes First and Last simply reuse the standard expansion
-
-      elsif Attr_Id = Attribute_First
-        or else Attr_Id = Attribute_Last
-      then
-         Exp_Attr.Expand_N_Attribute_Reference (N);
       end if;
    end Expand_SPARK_N_Attribute_Reference;