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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 6 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 1d790e7cd2..5dae389a62 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl)) | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) -| TTBigint -> MayRecNo (Aentry Prim.bigint) +| TTBigint -> MayRecNo (Aentry Prim.bignat) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with @@ -411,8 +411,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v))) end | TTReference -> begin match forpat with diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 22e4e35ad4..475d5c31f7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -252,7 +252,7 @@ let quote_notation_token x = let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - NumTok.of_string x <> None + NumTok.Unsigned.parse_string x <> None | _ -> false |