From 154aeaad0802e621d09048e1e32485946a3ec443 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jan 2020 00:54:06 +0100
Subject: When parsing negative integer, ensure minus sign is contiguous to the
 number.

For instance, formerly, "Set Inline Level - 1" was succeeding. Now
only "Set Inline Level -1" succeeds. (Even though -1 does not make
sense for a Inline Level, but that's then a semantic issue. Other
options may accept negative numbers in general.)
---
 parsing/g_prim.mlg | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 5f61b9a047..7e0360af72 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -37,6 +37,12 @@ let test_pipe_closedcurly =
     lk_kw "|" >> lk_kw "}" >> check_no_space
   end
 
+let test_minus_nat =
+  let open Pcoq.Lookahead in
+  to_entry "test_minus_nat" begin
+    lk_kw "-" >> lk_nat >> check_no_space
+  end
+
 }
 
 GRAMMAR EXTEND Gram
@@ -122,7 +128,7 @@ GRAMMAR EXTEND Gram
   ;
   integer:
     [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
-      | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
+      | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
   ;
   natural:
     [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
-- 
cgit v1.2.3