From 9ddae1778aef70c55a1347c4d0b28694cf34a5af Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 13:39:06 +0100
Subject: Fix some documentation typos.

---
 parsing/pcoq.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ec8dac8210..37165f6ceb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -39,7 +39,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
         |     (together with a constr entry level, e.g. 50, and indications of)
         |     (subentries, e.g. x in constr next level and y constr same level)
         |
-        | spliting into tokens by Metasyntax.split_notation_string
+        | splitting into tokens by Metasyntax.split_notation_string
         V
       [String "x"; String "+"; String "y"] : symbol_token list
         |
@@ -96,7 +96,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
 
 *)
 
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
@@ -232,14 +232,14 @@ type gram_reinit = gram_assoc * gram_position
 
 val grammar_extend : 'a Gram.entry -> gram_reinit option ->
   'a Extend.extend_statment -> unit
-(** Extend the grammar of Coq, without synchronizing it with the bactracking
+(** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
 
 (** {5 Extending the parser with summary-synchronized commands} *)
 
 module GramState : Store.S
-(** Auxilliary state of the grammar. Any added data must be marshallable. *)
+(** Auxiliary state of the grammar. Any added data must be marshallable. *)
 
 type 'a grammar_command
 (** Type of synchronized parsing extensions. The ['a] type should be
-- 
cgit v1.2.3


From 89fc7443d2e35f5020d272faecc4fe1f6e12eb11 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 11:37:24 +0100
Subject: Fix #5174: Underinformative syntax error messages in the new
 arguments syntax

We introduce a bit of compatibility parsing code to print deprecation
warnings.
---
 parsing/g_vernac.ml4 | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9b52d1bf31..e61be53a99 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,9 +582,9 @@ let warn_deprecated_implicit_arguments =
 
 let warn_deprecated_arguments_syntax =
   CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated"
-         (fun () -> strbrk "The \"/\" modifier has an effect only in the first "
-                    ++ strbrk "arguments list. The syntax allowing it to appear"
-                    ++ strbrk " in other lists is deprecated.")
+         (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only "
+                    ++ strbrk "in the first arguments list. The syntax allowing"
+                    ++ strbrk " them to appear in other lists is deprecated.")
 
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
@@ -664,8 +664,8 @@ GEXTEND Gram
         more_implicits = OPT
           [ ","; impl = LIST1
             [ impl = LIST0 more_implicits_block ->
-              let warn_slash = List.exists fst impl in
-              if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc ();
+              let warn_deprecated = List.exists fst impl in
+              if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc ();
               List.flatten (List.map snd impl)]
             SEP "," -> impl
           ];
@@ -776,14 +776,19 @@ GEXTEND Gram
                  implicit_status = MaximallyImplicit}) items
     ]
   ];
+  name_or_bang: [
+       [ b = OPT "!"; id = name ->
+       not (Option.is_empty b), id
+    ]
+  ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)])
+    [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)])
     | "/" -> (true (* Should warn about deprecated syntax *), [])
-    | "["; items = LIST1 name; "]" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items)
-    | "{"; items = LIST1 name; "}" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items)
+    | "["; items = LIST1 name_or_bang; "]" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items)
+    | "{"; items = LIST1 name_or_bang; "}" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items)
     ]
   ];
   strategy_level:
-- 
cgit v1.2.3