[multiple changes]

2014-08-01  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Resolve_Call): Do not perform
	GNATprove-specific inlining while within a generic.

2014-08-01  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Case_Expression): Handle properly a
	case expression with incompatible alternatives, when the first
	alternative is overloaded.

From-SVN: r213460

gcc/ada/ChangeLog

+2014-08-01  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Do not perform
+	GNATprove-specific inlining while within a generic.
+
+2014-08-01  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Analyze_Case_Expression): Handle properly a
+	case expression with incompatible alternatives, when the first
+	alternative is overloaded.
+
 2014-08-01  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_res.adb (Check_Parameterless_Call): Use Relocate_Node

gcc/ada/sem_ch4.adb

@@ -1363,6 +1363,9 @@ package body Sem_Ch4 is
       Others_Present : Boolean;
       --  Indicates if Others was present
 
+      Wrong_Alt : Node_Id;
+      --  For error reporting
+
    --  Start of processing for Analyze_Case_Expression
 
    begin
@@ -1415,6 +1418,9 @@ package body Sem_Ch4 is
 
                if No (Alt) then
                   Add_One_Interp (N, It.Typ, It.Typ);
+
+               else
+                  Wrong_Alt := Alt;
                end if;
 
                Get_Next_Interp (I, It);
@@ -1441,6 +1447,12 @@ package body Sem_Ch4 is
          return;
       end if;
 
+      if Etype (N) = Any_Type and then Present (Wrong_Alt) then
+         Error_Msg_N ("type incompatible with that of previous alternatives",
+           Expression (Wrong_Alt));
+         return;
+      end if;
+
       --  If the case expression is a formal object of mode in out, then
       --  treat it as having a nonstatic subtype by forcing use of the base
       --  type (which has to get passed to Check_Case_Choices below).  Also

gcc/ada/sem_res.adb

@@ -6208,14 +6208,15 @@ package body Sem_Res is
       Eval_Call (N);
       Check_Elab_Call (N);
 
-      --  In GNATprove mode, expansion is disabled, but we want to inline
-      --  some subprograms to facilitate formal verification. Indirect calls,
-      --  through a subprogram type, cannot be inlined. Inlining is only
-      --  performed for calls for which SPARK_Mode is On.
+      --  In GNATprove mode, expansion is disabled, but we want to inline some
+      --  subprograms to facilitate formal verification. Indirect calls through
+      --  a subprogram type or within a generic cannot be inlined. Inlining is
+      --  performed only for calls subject to SPARK_Mode on.
 
       if GNATprove_Mode
-        and then Is_Overloadable (Nam)
         and then SPARK_Mode = On
+        and then Is_Overloadable (Nam)
+        and then not Inside_A_Generic
       then
          --  Retrieve the body to inline from the ultimate alias of Nam, if
          --  there is one, otherwise calls that should be inlined end up not