diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 89848069514..e64b7badca6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Build_Body_To_Inline): Issue more precise messages
+	for declarations that prevent inlining.
+	(Cannot_Inline): Change usual start of message to refer to contextual
+	analysis in GNATprove mode.
+	* sem_res.adb (Resolve_Call): Change usual start of message to
+	refer to contextual analysis in GNATprove mode, when inlining
+	not possible.
+
 2014-07-30  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb, sem_ch6.adb: Minor code reorganization.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index f3a04debc81..65fec716974 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -923,17 +923,48 @@ package body Inline is
       begin
          D := First (Decls);
          while Present (D) loop
-            if (Nkind (D) = N_Function_Instantiation
-                 and then not Is_Unchecked_Conversion (D))
-              or else Nkind_In (D, N_Protected_Type_Declaration,
-                                   N_Package_Declaration,
-                                   N_Package_Instantiation,
-                                   N_Subprogram_Body,
-                                   N_Procedure_Instantiation,
-                                   N_Task_Type_Declaration)
+            if Nkind (D) = N_Function_Instantiation
+              and then not Is_Unchecked_Conversion (D)
             then
                Cannot_Inline
-                 ("cannot inline & (non-allowed declaration)?", D, Subp);
+                 ("cannot inline & (nested function instantiation)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Protected_Type_Declaration then
+               Cannot_Inline
+                 ("cannot inline & (nested protected type declaration)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Package_Declaration then
+               Cannot_Inline
+                 ("cannot inline & (nested package declaration)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Package_Instantiation then
+               Cannot_Inline
+                 ("cannot inline & (nested package instantiation)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Subprogram_Body then
+               Cannot_Inline
+                 ("cannot inline & (nested subprogram)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Procedure_Instantiation then
+               Cannot_Inline
+                 ("cannot inline & (nested procedure instantiation)?",
+                  D, Subp);
+               return True;
+
+            elsif Nkind (D) = N_Task_Type_Declaration then
+               Cannot_Inline
+                 ("cannot inline & (nested task type declaration)?",
+                  D, Subp);
                return True;
             end if;
 
@@ -1435,6 +1466,27 @@ package body Inline is
       Is_Serious : Boolean := False)
    is
    begin
+      --  In GNATprove mode, inlining is the technical means by which the
+      --  higher-level goal of contextual analysis is reached, so issue
+      --  messages about failure to apply contextual analysis to a
+      --  subprogram, rather than failure to inline it.
+
+      if GNATprove_Mode
+        and then Msg (Msg'First .. Msg'First + 12) = "cannot inline"
+      then
+         declare
+            Len1 : constant Positive := 13;  --  "cannot inline"
+            Len2 : constant Positive := 25;  --  "no contextual analysis of"
+            New_Msg : String (1 .. Msg'Length + Len2 - Len1);
+         begin
+            New_Msg (1 .. Len2) := "no contextual analysis of";
+            New_Msg (Len2 + 1 .. Msg'Length + Len2 - Len1) :=
+              Msg (Msg'First + Len1 .. Msg'Last);
+            Cannot_Inline (New_Msg, N, Subp, Is_Serious);
+            return;
+         end;
+      end if;
+
       pragma Assert (Msg (Msg'Last) = '?');
 
       --  Old semantics
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index f82548c67ab..43441248eb7 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6233,7 +6233,7 @@ package body Sem_Res is
             --  assertions as logic expressions.
 
             elsif In_Assertion_Expr /= 0 then
-               Error_Msg_NE ("?cannot inline call to &", N, Nam);
+               Error_Msg_NE ("?no contextual analysis of &", N, Nam);
                Error_Msg_N ("\call appears in assertion expression", N);
                Set_Is_Inlined_Always (Nam_UA, False);
 
@@ -6246,7 +6246,8 @@ package body Sem_Res is
 
                if No (Corresponding_Body (Decl)) then
                   Error_Msg_NE
-                    ("?cannot inline call to & (body not seen yet)", N, Nam);
+                    ("?no contextual analysis of & (body not seen yet)",
+                     N, Nam);
                   Set_Is_Inlined_Always (Nam_UA, False);
 
                --  Nothing to do if there is no body to inline, indicating that
@@ -6261,7 +6262,7 @@ package body Sem_Res is
                --  expressions, that are not handled by GNATprove.
 
                elsif Is_Potentially_Unevaluated (N) then
-                  Error_Msg_NE ("?cannot inline call to &", N, Nam);
+                  Error_Msg_NE ("?no contextual anlysis of &", N, Nam);
                   Error_Msg_N
                     ("\call appears in potentially unevaluated context", N);
                   Set_Is_Inlined_Always (Nam_UA, False);