From 0d06d69ffc0436ed326bf3e4c684dc17a4d85dde Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 12:43:46 +0100
Subject: Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.

---
 grammar/tacextend.mlp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index a1b3f4f255..683a7e2f71 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -48,7 +48,7 @@ let make_fun_clauses loc s l =
   let map c = GramCompat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
-let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
+let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
 
 let rec mlexpr_of_symbol = function
 | Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
-- 
cgit v1.2.3


From 5358515f23d1cd47d4914c55dcf049df858b9dc7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Nov 2016 16:46:34 +0100
Subject: Better Arguments compatibility.

With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
---
 parsing/g_vernac.ml4 | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e0d836df80..5e2856b2fc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -580,6 +580,12 @@ let warn_deprecated_implicit_arguments =
   CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated"
          (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead")
 
+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.")
+
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
   GLOBAL: gallina_ext instance_name;
@@ -654,7 +660,10 @@ GEXTEND Gram
         args = LIST0 argument_spec_block;
         more_implicits = OPT
           [ ","; impl = LIST1
-            [ impl = LIST0 more_implicits_block -> List.flatten impl]
+            [ impl = LIST0 more_implicits_block ->
+              let warn_slash = List.exists fst impl in
+              if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc ();
+              List.flatten (List.map snd impl)]
             SEP "," -> impl
           ];
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
@@ -766,11 +775,12 @@ GEXTEND Gram
   ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
+    [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)])
+    | "/" -> (true (* Should warn about deprecated syntax *), [])
     | "["; items = LIST1 name; "]" ->
-       List.map (fun name -> (snd name, Vernacexpr.Implicit)) items
+       (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items)
     | "{"; items = LIST1 name; "}" ->
-       List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items
+       (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items)
     ]
   ];
   strategy_level:
-- 
cgit v1.2.3


From 6b99de706e37c75407373e756e24f2256b848815 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 Nov 2016 09:45:49 +0100
Subject: Revert "Better Arguments compatibility."

This reverts commit 5358515f23d1cd47d4914c55dcf049df858b9dc7.

The syntax is deprecated in 8.6, so we now remove it from trunk.
---
 parsing/g_vernac.ml4 | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 71d16d682a..7bc5bfca38 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -580,12 +580,6 @@ let warn_deprecated_implicit_arguments =
   CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated"
          (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead")
 
-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.")
-
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
   GLOBAL: gallina_ext instance_name;
@@ -660,10 +654,7 @@ GEXTEND Gram
         args = LIST0 argument_spec_block;
         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 ();
-              List.flatten (List.map snd impl)]
+            [ impl = LIST0 more_implicits_block -> List.flatten impl]
             SEP "," -> impl
           ];
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
@@ -775,12 +766,11 @@ GEXTEND Gram
   ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)])
-    | "/" -> (true (* Should warn about deprecated syntax *), [])
+    [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
     | "["; items = LIST1 name; "]" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items)
+       List.map (fun name -> (snd name, Vernacexpr.Implicit)) items
     | "{"; items = LIST1 name; "}" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items)
+       List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items
     ]
   ];
   strategy_level:
-- 
cgit v1.2.3