Merge PR #12218: Numeral notations for non inductive types

Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48

1 files changed, 179 insertions, 81 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index c150ae7abb..8d05fab63c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -32,7 +32,7 @@ open NumTok
     fail if a number has no interpretation in the scope (e.g. there is
     no interpretation for negative numbers in [nat]); interpreters both for
     terms and patterns can be set; these interpreters are in permanent table
-    [numeral_interpreter_tab]
+    [number_interpreter_tab]
   - a set of ML printers for expressions denoting numbers parsable in
     this scope
   - a set of interpretations for infix (more generally distfix) notations
@@ -451,13 +451,13 @@ module InnerPrimToken = struct
 
   let do_interp ?loc interp primtok =
     match primtok, interp with
-    | Numeral n, RawNumInterp interp -> interp ?loc n
-    | Numeral n, BigNumInterp interp ->
+    | Number n, RawNumInterp interp -> interp ?loc n
+    | Number n, BigNumInterp interp ->
       (match NumTok.Signed.to_bigint n with
        | Some n -> interp ?loc n
        | None -> raise Not_found)
     | String s, StringInterp interp -> interp ?loc s
-    | (Numeral _ | String _),
+    | (Number _ | String _),
       (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
 
   type uninterpreter =
@@ -471,16 +471,16 @@ module InnerPrimToken = struct
     | StringUninterp f, StringUninterp f' -> f == f'
     | _ -> false
 
-  let mkNumeral n =
-    Numeral (NumTok.Signed.of_bigint CDec n)
+  let mkNumber n =
+    Number (NumTok.Signed.of_bigint CDec n)
 
   let mkString = function
     | None -> None
     | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
   let do_uninterp uninterp g = match uninterp with
-    | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
-    | BigNumUninterp u -> Option.map mkNumeral (u g)
+    | RawNumUninterp u -> Option.map (fun (s,n) -> Number (s,n)) (u g)
+    | BigNumUninterp u -> Option.map mkNumber (u g)
     | StringUninterp u -> mkString (u g)
 
 end
@@ -500,7 +500,7 @@ let prim_token_uninterpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
 
 (*******************************************************)
-(* Numeral notation interpretation                     *)
+(* Number notation interpretation                      *)
 type prim_token_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
@@ -524,21 +524,21 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
-type numeral_ty =
+type number_ty =
   { int : int_ty;
     decimal : Names.inductive;
     hexadecimal : Names.inductive;
-    numeral : Names.inductive }
+    number : Names.inductive }
 
 type target_kind =
-  | Int of int_ty (* Coq.Init.Numeral.int + uint *)
-  | UInt of int_ty (* Coq.Init.Numeral.uint *)
+  | Int of int_ty (* Coq.Init.Number.int + uint *)
+  | UInt of int_ty (* Coq.Init.Number.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
-  | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+  | Number of number_ty (* Coq.Init.Number.number + uint + int *)
   | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
   | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
@@ -547,19 +547,36 @@ type string_target_kind =
 type option_kind = Option | Direct
 type 'target conversion_kind = 'target * option_kind
 
+(** A postprocessing translation [to_post] can be done after execution
+   of the [to_ty] interpreter. The reverse translation is performed
+   before the [of_ty] uninterpreter.
+
+   [to_post] is an array of [n] lists [l_i] of tuples [(f, t,
+   args)]. When the head symbol of the translated term matches one of
+   the [f] in the list [l_0] it is replaced by [t] and its arguments
+   are translated acording to [args] where [ToPostCopy] means that the
+   argument is kept unchanged and [ToPostAs k] means that the
+   argument is recursively translated according to [l_k].
+   [ToPostHole] introduces an additional implicit argument hole
+   (in the reverse translation, the corresponding argument is removed).
+   [ToPostCheck r] behaves as [ToPostCopy] except in the reverse
+   translation which fails if the copied term is not [r].
+   When [n] is null, no translation is performed. *)
+type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t
 type ('target, 'warning) prim_token_notation_obj =
   { to_kind : 'target conversion_kind;
     to_ty : GlobRef.t;
+    to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array;
     of_kind : 'target conversion_kind;
     of_ty : GlobRef.t;
     ty_name : Libnames.qualid; (* for warnings / error messages *)
     warning : 'warning }
 
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
 type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
 
 module PrimTokenNotation = struct
-(** * Code shared between Numeral notation and String notation *)
+(** * Code shared between Number notation and String notation *)
 (** Reduction
 
     The constr [c] below isn't necessarily well-typed, since we
@@ -593,22 +610,69 @@ exception NotAValidPrimToken
     to [constr] for the subset that concerns us.
 
     Note that if you update [constr_of_glob], you should update the
-    corresponding numeral notation *and* string notation doc in
+    corresponding number notation *and* string notation doc in
     doc/sphinx/user-extensions/syntax-extensions.rst that describes
     what it means for a term to be ground / to be able to be
     considered for parsing. *)
 
-let rec constr_of_glob env sigma g = match DAst.get g with
-  | Glob_term.GRef (GlobRef.ConstructRef c, _) ->
-      let sigma,c = Evd.fresh_constructor_instance env sigma c in
-      sigma,mkConstructU c
-  | Glob_term.GRef (GlobRef.IndRef c, _) ->
-      let sigma,c = Evd.fresh_inductive_instance env sigma c in
-      sigma,mkIndU c
+let constr_of_globref allow_constant env sigma = function
+  | GlobRef.ConstructRef c ->
+     let sigma,c = Evd.fresh_constructor_instance env sigma c in
+     sigma,mkConstructU c
+  | GlobRef.IndRef c ->
+     let sigma,c = Evd.fresh_inductive_instance env sigma c in
+     sigma,mkIndU c
+  | GlobRef.ConstRef c when allow_constant ->
+     let sigma,c = Evd.fresh_constant_instance env sigma c in
+     sigma,mkConstU c
+  | _ -> raise NotAValidPrimToken
+
+let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get g with
+  | Glob_term.GRef (r, _) ->
+      let o = List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post in
+      begin match o with
+      | None -> constr_of_globref allow_constant env sigma r
+      | Some (r, _, a) ->
+         (* [g] is not a GApp so check that [post]
+            does not expect any actual argument
+            (i.e., [a] contains only ToPostHole since they mean "ignore arg") *)
+         if List.exists ((<>) ToPostHole) a then raise NotAValidPrimToken;
+         constr_of_globref true env sigma r
+      end
   | Glob_term.GApp (gc, gcl) ->
-      let sigma,c = constr_of_glob env sigma gc in
-      let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
-      sigma,mkApp (c, Array.of_list cl)
+      let o = match DAst.get gc with
+        | Glob_term.GRef (r, _) -> List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post
+        | _ -> None in
+      begin match o with
+      | None ->
+         let sigma,c = constr_of_glob allow_constant to_post post env sigma gc in
+         let sigma,cl = List.fold_left_map (constr_of_glob allow_constant to_post post env) sigma gcl in
+         sigma,mkApp (c, Array.of_list cl)
+      | Some (r, _, a) ->
+         let sigma,c = constr_of_globref true env sigma r in
+         let rec aux sigma a gcl = match a, gcl with
+           | [], [] -> sigma,[]
+           | ToPostCopy :: a, gc :: gcl ->
+              let sigma,c = constr_of_glob allow_constant [||] [] env sigma gc in
+              let sigma,cl = aux sigma a gcl in
+              sigma, c :: cl
+           | ToPostCheck r :: a, gc :: gcl ->
+              let () = match DAst.get gc with
+                | Glob_term.GRef (r', _) when GlobRef.equal r r' -> ()
+                | _ -> raise NotAValidPrimToken in
+              let sigma,c = constr_of_glob true [||] [] env sigma gc in
+              let sigma,cl = aux sigma a gcl in
+              sigma, c :: cl
+           | ToPostAs i :: a, gc :: gcl ->
+              let sigma,c = constr_of_glob allow_constant to_post to_post.(i) env sigma gc in
+              let sigma,cl = aux sigma a gcl in
+              sigma, c :: cl
+           | ToPostHole :: post, _ :: gcl -> aux sigma post gcl
+           | [], _ :: _ | _ :: _, [] -> raise NotAValidPrimToken
+         in
+         let sigma,cl = aux sigma a gcl in
+         sigma,mkApp (c, Array.of_list cl)
+      end
   | Glob_term.GInt i -> sigma, mkInt i
   | Glob_term.GSort gs ->
       let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
@@ -616,6 +680,10 @@ let rec constr_of_glob env sigma g = match DAst.get g with
   | _ ->
       raise NotAValidPrimToken
 
+let constr_of_glob to_post env sigma (Glob_term.AnyGlobConstr g) =
+  let post = match to_post with [||] -> [] | _ -> to_post.(0) in
+  constr_of_glob false to_post post env sigma g
+
 let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | App (c, ca) ->
       let c = glob_of_constr token_kind ?loc env sigma c in
@@ -637,9 +705,38 @@ let no_such_prim_token uninterpreted_token_kind ?loc ty =
    (str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++
     pr_qualid ty)
 
-let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c =
+let rec postprocess token_kind ?loc ty to_post post g =
+  let g', gl = match DAst.get g with Glob_term.GApp (g, gl) -> g, gl | _ -> g, [] in
+  let o =
+    match DAst.get g' with
+    | Glob_term.GRef (r, None) ->
+       List.find_opt (fun (r',_,_) -> GlobRef.equal r r') post
+    | _ -> None in
+  match o with None -> g | Some (_, r, a) ->
+  let rec f n a gl = match a, gl with
+    | [], [] -> []
+    | ToPostHole :: a, gl ->
+       let e = Evar_kinds.ImplicitArg (r, (n, None), true) in
+       let h = DAst.make ?loc (Glob_term.GHole (e, Namegen.IntroAnonymous, None)) in
+       h :: f (n+1) a gl
+    | (ToPostCopy | ToPostCheck _) :: a, g :: gl -> g :: f (n+1) a gl
+    | ToPostAs c :: a, g :: gl ->
+       postprocess token_kind ?loc ty to_post to_post.(c) g :: f (n+1) a gl
+    | [], _::_ | _::_, [] ->
+       no_such_prim_token token_kind ?loc ty
+  in
+  let gl = f 1 a gl in
+  let g = DAst.make ?loc (Glob_term.GRef (r, None)) in
+  DAst.make ?loc (Glob_term.GApp (g, gl))
+
+let glob_of_constr token_kind ty ?loc env sigma to_post c =
+  let g = glob_of_constr token_kind ?loc env sigma c in
+  match to_post with [||] -> g | _ ->
+    postprocess token_kind ?loc ty to_post to_post.(0) g
+
+let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma to_post c =
   match Constr.kind c with
-  | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c
+  | App (_Some, [| _; c |]) -> glob_of_constr token_kind ty ?loc env sigma to_post c
   | App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty
   | x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c))
 
@@ -648,13 +745,13 @@ let uninterp_option c =
   | App (_Some, [| _; x |]) -> x
   | _ -> raise NotAValidPrimToken
 
-let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
+let uninterp to_raw o n =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
   let of_ty = EConstr.Unsafe.to_constr of_ty in
   try
-    let sigma,n = constr_of_glob env sigma n in
+    let sigma,n = constr_of_glob o.to_post env sigma n in
     let c = eval_constr_app env sigma of_ty n in
     let c = if snd o.of_kind == Direct then c else uninterp_option c in
     Some (to_raw (fst o.of_kind, c))
@@ -675,8 +772,8 @@ let rec int63_of_pos_bigint i =
       (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
     else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
 
-module Numeral = struct
-(** * Numeral notation *)
+module Numbers = struct
+(** * Number notation *)
 open PrimTokenNotation
 
 let warn_large_num =
@@ -732,7 +829,7 @@ let coqint_of_rawnum inds c (sign,n) =
   let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
   mkApp (mkConstruct (ind, pos_neg), [|uint|])
 
-let coqnumeral_of_rawnum inds c n =
+let coqnumber_of_rawnum inds c n =
   let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in
   let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in
   let i = coqint_of_rawnum inds.int c i in
@@ -744,19 +841,19 @@ let coqnumeral_of_rawnum inds c n =
     mkApp (mkConstruct (ind, 2), [|i; f; e|])  (* (D|Hexad)ecimalExp *)
 
 let mkDecHex ind c n = match c with
-  | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Dec *)
-  | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hex *)
+  | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Decimal *)
+  | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hexadecimal *)
 
 exception NonDecimal
 
-let decimal_coqnumeral_of_rawnum inds n =
+let decimal_coqnumber_of_rawnum inds n =
   if NumTok.Signed.classify n <> CDec then raise NonDecimal;
-  coqnumeral_of_rawnum inds CDec n
+  coqnumber_of_rawnum inds CDec n
 
-let coqnumeral_of_rawnum inds n =
+let coqnumber_of_rawnum inds n =
   let c = NumTok.Signed.classify n in
-  let n = coqnumeral_of_rawnum inds c n in
-  mkDecHex inds.numeral c n
+  let n = coqnumber_of_rawnum inds c n in
+  mkDecHex inds.number c n
 
 let decimal_coquint_of_rawnum inds n =
   if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
@@ -806,7 +903,7 @@ let rawnum_of_coqint cl c =
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let rawnum_of_coqnumeral cl c =
+let rawnum_of_coqnumber cl c =
   let of_ife i f e =
     let n = rawnum_of_coqint cl i in
     let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
@@ -820,17 +917,17 @@ let rawnum_of_coqnumeral cl c =
 let destDecHex c = match Constr.kind c with
   | App (c,[|c'|]) ->
      (match Constr.kind c with
-      | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c'
-      | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c'
+      | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c'
+      | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c'
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let decimal_rawnum_of_coqnumeral c =
-  rawnum_of_coqnumeral CDec c
+let decimal_rawnum_of_coqnumber c =
+  rawnum_of_coqnumber CDec c
 
-let rawnum_of_coqnumeral c =
+let rawnum_of_coqnumber c =
   let cl, c = destDecHex c in
-  rawnum_of_coqnumeral cl c
+  rawnum_of_coqnumber cl c
 
 let decimal_rawnum_of_coquint c =
   rawnum_of_coquint CDec c
@@ -952,9 +1049,9 @@ let interp o ?loc n =
        interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
     | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
        no_such_prim_token "number" ?loc o.ty_name
-    | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
-    | Decimal numeral_ty, _ ->
-       (try decimal_coqnumeral_of_rawnum numeral_ty n
+    | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
+    | Decimal number_ty, _ ->
+       (try decimal_coqnumber_of_rawnum number_ty n
         with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
   in
   let env = Global.env () in
@@ -964,12 +1061,13 @@ let interp o ?loc n =
   match o.warning, snd o.to_kind with
   | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
-     glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
+     assert (Array.length o.to_post = 0);
+     glob_of_constr "number" o.ty_name ?loc env sigma o.to_post (mkApp (to_ty,[|c|]))
   | _ ->
      let res = eval_constr_app env sigma to_ty c in
      match snd o.to_kind with
-     | Direct -> glob_of_constr "numeral" ?loc env sigma res
-     | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+     | Direct -> glob_of_constr "number" o.ty_name ?loc env sigma o.to_post res
+     | Option -> interp_option "number" "number" o.ty_name ?loc env sigma o.to_post res
 
 let uninterp o n =
   PrimTokenNotation.uninterp
@@ -978,10 +1076,10 @@ let uninterp o n =
       | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
       | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
       | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
-      | (Numeral _, c) -> rawnum_of_coqnumeral c
+      | (Number _, c) -> rawnum_of_coqnumber c
       | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
       | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
-      | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c
+      | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
     end o n
 end
 
@@ -1014,11 +1112,12 @@ let coqbyte_of_string ?loc byte s =
   let p =
     if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
-      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
-      then int_of_string s
-      else
+      let n =
+        if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+        then int_of_string s else 256 in
+      if n < 256 then n else
        user_err ?loc ~hdr:"coqbyte_of_string"
-         (str "Expects a single character or a three-digits ascii code.") in
+         (str "Expects a single character or a three-digit ASCII code.") in
   coqbyte_of_char_code byte p
 
 let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
@@ -1073,8 +1172,8 @@ let interp o ?loc n =
   let to_ty = EConstr.Unsafe.to_constr to_ty in
   let res = eval_constr_app env sigma to_ty c in
   match snd o.to_kind with
-  | Direct -> glob_of_constr "string" ?loc env sigma res
-  | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res
+  | Direct -> glob_of_constr "string" o.ty_name ?loc env sigma o.to_post res
+  | Option -> interp_option "string" "string" o.ty_name ?loc env sigma o.to_post res
 
 let uninterp o n =
   PrimTokenNotation.uninterp
@@ -1086,21 +1185,21 @@ end
 
 (* A [prim_token_infos], which is synchronized with the document
    state, either contains a unique id pointing to an unsynchronized
-   prim token function, or a numeral notation object describing how to
+   prim token function, or a number notation object describing how to
    interpret and uninterpret.  We provide [prim_token_infos] because
    we expect plugins to provide their own interpretation functions,
-   rather than going through numeral notations, which are available as
+   rather than going through number notations, which are available as
    a vernacular. *)
 
 type prim_token_interp_info =
     Uid of prim_token_uid
-  | NumeralNotation of numeral_notation_obj
+  | NumberNotation of number_notation_obj
   | StringNotation of string_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -1124,7 +1223,7 @@ let hashtbl_check_and_set allow_overwrite uid f h eq =
    | _ ->
       user_err ~hdr:"prim_token_interpreter"
        (str "Unique identifier " ++ str uid ++
-        str " already used to register a numeral or string (un)interpreter.")
+        str " already used to register a number or string (un)interpreter.")
 
 let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
   hashtbl_check_and_set
@@ -1152,7 +1251,6 @@ let cache_prim_token_interpretation (_,infos) =
     String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
   let add_uninterp r =
     let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
-    let l = List.remove_assoc_f String.equal sc l in
     prim_token_uninterp_infos :=
       GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
         !prim_token_uninterp_infos in
@@ -1225,7 +1323,7 @@ let check_required_module ?loc sc (sp,d) =
         (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
          str (List.last d) ++ str ".")
 
-(* Look if some notation or numeral printer in [scope] can be used in
+(* Look if some notation or number printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
 let find_with_delimiters = function
@@ -1242,7 +1340,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       | NotationInScope scope' when String.equal scope scope' ->
         Some (None,None)
       | _ ->
-        (* If the most recently open scope has a notation/numeral printer
+        (* If the most recently open scope has a notation/number printer
            but not the expected one then we need delimiters *)
         if find scope then
           find_with_delimiters ntn_scope
@@ -1380,8 +1478,8 @@ let find_notation ntn sc =
   | _ -> raise Not_found
 
 let notation_of_prim_token = function
-  | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
-  | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
+  | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+  | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -1399,7 +1497,7 @@ let find_prim_token check_allowed ?loc p sc =
   check_required_module ?loc sc spdir;
   let interp = match info with
     | Uid uid -> Hashtbl.find prim_token_interpreters uid
-    | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+    | NumberNotation o -> InnerPrimToken.RawNumInterp (Numbers.interp o)
     | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
   in
   let pat = InnerPrimToken.do_interp ?loc interp p in
@@ -1416,8 +1514,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
     let _, info = Exninfo.capture exn in
     user_err ?loc ~info ~hdr:"interp_prim_token"
     ((match p with
-      | Numeral _ ->
-         str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
+      | Number _ ->
+         str "No interpretation for number " ++ pr_notation (notation_of_prim_token p)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token ?loc =
@@ -1667,14 +1765,14 @@ let availability_of_prim_token n printer_scope local_scopes =
       let uid = snd (String.Map.find scope !prim_token_interp_infos) in
       let open InnerPrimToken in
       match n, uid with
-      | Constrexpr.Numeral _, NumeralNotation _ -> true
-      | _, NumeralNotation _ -> false
+      | Constrexpr.Number _, NumberNotation _ -> true
+      | _, NumberNotation _ -> false
       | String _, StringNotation _ -> true
       | _, StringNotation _ -> false
       | _, Uid uid ->
         let interp = Hashtbl.find prim_token_interpreters uid in
         match n, interp with
-        | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+        | Constrexpr.Number _, (RawNumInterp _ | BigNumInterp _) -> true
         | String _, StringInterp _ -> true
         | _ -> false
     with Not_found -> false
@@ -1689,7 +1787,7 @@ let rec find_uninterpretation need_delim def find = function
         def
   | OpenScopeItem scope :: scopes ->
       (try find need_delim scope
-       with Not_found -> find_uninterpretation need_delim def find scopes)  (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+       with Not_found -> find_uninterpretation need_delim def find scopes)  (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a number notation *)
   | LonelyNotationItem ntn::scopes ->
       find_uninterpretation (ntn::need_delim) def find scopes
 
@@ -1701,7 +1799,7 @@ let uninterp_prim_token c local_scopes =
        try
          let uninterp = match info with
            | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
-           | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+           | NumberNotation o -> InnerPrimToken.RawNumUninterp (Numbers.uninterp o)
            | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
          in
          match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with