From 0c268f5363ce7f72e85626b73082012b4e879d74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Oct 2017 17:57:29 +0100
Subject: Improving checks about the list separator in tactic notations.

In Tactic Notation and TACTIC EXTEND, when an argument not ending with
"_list_sep" was given with a separator, the separator was silently
ignored.

Now:
- we take it into account if it is a list (i.e. ending with "_list"), as if
  "_list_sep" was given, since after all, the "_sep" is useless in the name.
- we fail if there is a separator but it is not a "_list" or "_list_sep".
---
 grammar/q_util.mlp | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'grammar')

diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 536ee7ca56..c2d767396a 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -94,10 +94,14 @@ let coincide s pat off =
   done;
   !break
 
+let check_separator sep =
+  if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep."
+
 let rec parse_user_entry s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
     let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    check_separator sep;
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
@@ -105,16 +109,20 @@ let rec parse_user_entry s sep =
     Ulist1sep (entry, sep)
   else if l > 5 && coincide s "_list" (l-5) then
     let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    check_separator sep;
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
     let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
     Ulist0sep (entry, sep)
   else if l > 4 && coincide s "_opt" (l-4) then
     let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    check_separator sep;
     Uopt entry
   else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
+    check_separator sep;
     Uentryl ("tactic", n)
   else
     let s = match s with "hyp" -> "var" | _ -> s in
+    check_separator sep;
     Uentry s
-- 
cgit v1.2.3


From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Nov 2017 22:54:24 +0100
Subject: Using a specific function to register vernac printers.

---
 grammar/argextend.mlp | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 12b7b171b7..9742a002d7 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl =
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
         Genarg.create_arg $se$ >>;
      make_extend loc s cl wit;
-    <:str_item< do {
-      Pptactic.declare_extra_genarg_pprule $wit$
-        $pr_rules$
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer."))
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) }
-      >> ]
+    <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ]
 
 open Pcaml
 
-- 
cgit v1.2.3