[multiple changes]

2013-10-10  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Refined_Pre and Refined_Post are now allowed as
	assertion identifiers for pragma Assertion_Policy.
	* sem_prag.adb (Is_Valid_Assertion_Kind): Add Refined_Pre/Refined_Post
	* sem_ch13.adb: Minor reformatting.

2013-10-10  Pascal Obry  <obry@adacore.com>

	* prj-conf.adb: Code refactoring.

From-SVN: r203361

gcc/ada/ChangeLog

+2013-10-10  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Refined_Pre and Refined_Post are now allowed as
+	assertion identifiers for pragma Assertion_Policy.
+	* sem_prag.adb (Is_Valid_Assertion_Kind): Add Refined_Pre/Refined_Post
+	* sem_ch13.adb: Minor reformatting.
+
+2013-10-10  Pascal Obry  <obry@adacore.com>
+
+	* prj-conf.adb: Code refactoring.
+
 2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* einfo.adb: Remove Integrity_Level from the node usage list.

gcc/ada/gnat_rm.texi

@@ -1375,7 +1375,9 @@ ID_ASSERTION_KIND ::= Assertions           |
                       Loop_Variant         |
                       Postcondition        |
                       Precondition         |
-                      Predicate
+                      Predicate            |
+                      Refined_Post         |
+                      Refined_Pre          |
                       Statement_Assertions
 
 POLICY_IDENTIFIER ::= Check | Disable | Ignore

gcc/ada/sem_ch13.adb

@@ -1383,9 +1383,8 @@ package body Sem_Ch13 is
 
                pragma Assert (not Is_Disabled (Aspect));
 
-               --  Certan aspects allow for an optional name or expression. Do
-               --  not generate a pragma with an empty argument association
-               --  list.
+               --  Certain aspects allow for an optional name or expression. Do
+               --  not generate a pragma with empty argument association list.
 
                if No (Args) or else No (Expression (First (Args))) then
                   Args := No_List;

gcc/ada/sem_prag.adb

@@ -9127,10 +9127,10 @@ package body Sem_Prag is
          --                        Postcondition        |
          --                        Precondition         |
          --                        Predicate            |
+         --                        Refined_Post         |
+         --                        Refined_Pre          |
          --                        Statement_Assertions
 
-         --  Shouldn't Refined_Pre be in this list???
-
          --  Note: The RM_ASSERTION_KIND list is language-defined, and the
          --  ID_ASSERTION_KIND list contains implementation-defined additions
          --  recognized by GNAT. The effect is to control the behavior of
@@ -19482,6 +19482,8 @@ package body Sem_Prag is
             Name_Postcondition        |
             Name_Precondition         |
             Name_Predicate            |
+            Name_Refined_Post         |
+            Name_Refined_Pre          |
             Name_Statement_Assertions => return True;
 
          when others                  => return False;