[multiple changes]

2013-01-02  Vincent Celier  <celier@adacore.com>

	* usage.adb: Minor reformatting.

2013-01-02  Arnaud Charlet  <charlet@adacore.com>

	* opt.ads: Fix typo.

2013-01-02  Thomas Quinot  <quinot@adacore.com>

	* par_sco.adb: Generate P decision SCOs for SPARK pragmas
	Assume and Loop_Invariant.

From-SVN: r194791

gcc/ada/ChangeLog

+2013-01-02  Vincent Celier  <celier@adacore.com>
+
+	* usage.adb: Minor reformatting.
+
+2013-01-02  Arnaud Charlet  <charlet@adacore.com>
+
+	* opt.ads: Fix typo.
+
+2013-01-02  Thomas Quinot  <quinot@adacore.com>
+
+	* par_sco.adb: Generate P decision SCOs for SPARK pragmas
+	Assume and Loop_Invariant.
+
 2013-01-02  Robert Dewar  <dewar@adacore.com>
 
 	* vms_data.ads: Add entry for Float_Check_Valid (-gnateF).

gcc/ada/opt.ads

@@ -281,7 +281,7 @@ package Opt is
    --  Set to True to check that operations on predefined unconstrained float
    --  types (e.g. Float, Long_Float) do not overflow and generate infinities
    --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
-   --  of the -gnateo switch.
+   --  of the -gnateF switch.
 
    Check_Object_Consistency : Boolean := False;
    --  GNATBIND, GNATMAKE
@@ -1737,7 +1737,7 @@ package Opt is
    --  Set to True to check that operations on predefined unconstrained float
    --  types (e.g. Float, Long_Float) do not overflow and generate infinities
    --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
-   --  of the -gnateo switch.
+   --  of the -gnateF switch.
 
    Check_Policy_List_Config : Node_Id;
    --  GNAT

gcc/ada/par_sco.adb

@@ -1890,10 +1890,13 @@ package body Par_SCO is
 
                begin
                   case Nam is
-                     when Name_Assert        |
-                          Name_Check         |
-                          Name_Precondition  |
-                          Name_Postcondition =>
+                     when Name_Assert         |
+                          Name_Assert_And_Cut |
+                          Name_Assume         |
+                          Name_Check          |
+                          Name_Loop_Invariant |
+                          Name_Precondition   |
+                          Name_Postcondition  =>
 
                         --  For Assert/Check/Precondition/Postcondition, we
                         --  must generate a P entry for the decision. Note

gcc/ada/usage.adb

@@ -170,7 +170,7 @@ begin
    --  Line for -gnatea switch
 
    Write_Switch_Char ("ea");
-   Write_Line ("Delimiter for automatically added switches (internal switch");
+   Write_Line ("Delimiter for automatically added switches (internal switch)");
 
    --  Line for -gnateA switch
 
@@ -255,7 +255,7 @@ begin
    --  Line for -gnatez switch
 
    Write_Switch_Char ("ez");
-   Write_Line ("Delimiter for automatically added switches (internal switch");
+   Write_Line ("Delimiter for automatically added switches (internal switch)");
 
    --  Line for -gnatE switch