From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Oct 2018 13:16:25 +0200
Subject: Replace type sign = bool with SPlus | SMinus

---
 plugins/ltac/g_tactic.mlg | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..574e22d50e 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+  Numeral ((if 0<=n then SPlus else SMinus),string_of_int (abs n))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
-- 
cgit v1.2.3


From a95aacce6cc32726b494d4cc694da49eae86cf96 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 11:19:28 +0200
Subject: Rename the INT token to NUMERAL

In anticipation of future uses of this token for non integer numerals.
---
 plugins/ltac/g_tactic.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 574e22d50e..90dda4850e 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
-              | IDENT _ | INT _ ->
+              | IDENT _ | NUMERAL _ ->
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
-- 
cgit v1.2.3


From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 14:40:23 +0200
Subject: Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.
---
 plugins/ltac/g_tactic.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 90dda4850e..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -148,7 +148,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | _ -> ElimOnConstr clbind
 
 let mkNumeral n =
-  Numeral ((if 0<=n then SPlus else SMinus),string_of_int (abs n))
+  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
-- 
cgit v1.2.3