diff options
| author | coqbot-app[bot] | 2021-02-27 10:06:39 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-27 10:06:39 +0000 |
| commit | 3915bc904fc16060c25baaf7d5626e3587ad2891 (patch) | |
| tree | 81c21fc95c1790250396119583a57ef4b6f1f3a1 /interp/constrextern.ml | |
| parent | 1e54fe53ac47f08d7b8f13df16487b5a2639404f (diff) | |
| parent | 4302a75d82b9ac983cd89dd01c742c36777d921b (diff) | |
Merge PR #13559: Signed primitive integers
Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8138b4c6d9..4fb7861ca6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -969,7 +969,13 @@ let rec extern inctx ?impargs scopes vars r = with No_match -> extern inctx scopes vars r') | None -> - try extern_notations inctx scopes vars None r + let r' = match DAst.get r with + | GInt i when Coqlib.has_ref "num.int63.wrap_int" -> + let wrap = Coqlib.lib_ref "num.int63.wrap_int" in + DAst.make (GApp (DAst.make (GRef (wrap, None)), [r])) + | _ -> r in + + try extern_notations inctx scopes vars None r' with No_match -> let loc = r.CAst.loc in @@ -1123,7 +1129,7 @@ let rec extern inctx ?impargs scopes vars r = | GInt i -> extern_prim_token_delimiter_if_required - (Number (NumTok.Signed.of_int_string (Uint63.to_string i))) + (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i)))) "int63" "int63_scope" (snd scopes) | GFloat f -> extern_float f (snd scopes) |