diff options
| author | Pierre-Marie Pédrot | 2020-03-24 17:10:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-24 17:10:56 +0100 |
| commit | bc70bb31c579b9482d0189f20806632c62b26a61 (patch) | |
| tree | 8d7f505224ba9de5b3025d302239a929e1da68b6 /plugins/syntax/g_numeral.mlg | |
| parent | 9f1f56e04fab689ab05339f8cddea4bd2935a554 (diff) | |
| parent | 5d1c4ae7b8931c7a1dec5f61c2571919319aeb4a (diff) | |
Merge PR #11703: Making of NumTok an API for numeral
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: proux01
Diffstat (limited to 'plugins/syntax/g_numeral.mlg')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 49d29e7b63..e66dbe17b2 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -21,16 +21,16 @@ open Pcoq.Prim let pr_numnot_option = function | Nop -> mt () - | Warning n -> str "(warning after " ++ str n ++ str ")" - | Abstract n -> str "(abstract after " ++ str n ++ str ")" + | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" + | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" } VERNAC ARGUMENT EXTEND numnotoption PRINTED BY { pr_numnot_option } | [ ] -> { Nop } -| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } -| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF |