Fix pretty-printing of primitive integers

A scope delimiter was missing for primitive integers constants.

Add related regression tests.

3 files changed, 41 insertions, 1 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24b1362e6d..68791f85aa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -738,6 +738,14 @@ let extern_optimal extern r r' =
   | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
   | _ -> raise No_match
 
+(* Helper function for safe and optimal printing of primitive tokens  *)
+(* such as those for Int63                                            *)
+let extern_prim_token_delimiter_if_required n key_n scope_n scopes =
+  match availability_of_prim_token n scope_n scopes with
+  | Some None -> CPrim n
+  | None -> CDelimiters(key_n, CAst.make (CPrim n))
+  | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n))
+
 (**********************************************************************)
 (* mapping decl                                                       *)
 
@@ -967,8 +975,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
+
   | GInt i ->
-     CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+     extern_prim_token_delimiter_if_required
+       (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+       "int63" "int63_scope" (snd scopes)
 
   in insert_coercion coercion (CAst.make ?loc c)
 
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index fdd5599565..4d76f1210b 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,3 +1,7 @@
+2%int63
+     : int
+(2 + 2)%int63
+     : int
 2
      : int
 9223372036854775807
@@ -14,3 +18,15 @@ The command has indeed failed with message:
 int63 are only non-negative numbers.
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+2
+     : nat
+2%int63
+     : int
+t = 2%i63
+     : int
+t = 2%i63
+     : int
+2
+     : nat
+2
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 3dc364eddb..0385e529bf 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,5 +1,7 @@
 Require Import Int63 Cyclic63.
 
+Check 2%int63.
+Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
@@ -9,4 +11,15 @@ Eval vm_compute in 2+2.
 Eval vm_compute in 65675757 * 565675998.
 Fail Check -1.
 Fail Check 9223372036854775808.
+Open Scope nat_scope.
+Check 2. (* : nat *)
+Check 2%int63.
+Delimit Scope int63_scope with i63.
+Definition t := 2%int63.
+Print t.
+Delimit Scope nat_scope with int63.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
 Close Scope int63_scope.