Skip to content

Make type Notation.prim_token_uid private #20911

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 1 commit into from
Jul 17, 2025
Merged

Make type Notation.prim_token_uid private #20911

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions dev/ci/user-overlays/20911-SkySkimmer-notation-uid.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
overlay bignums https://github.com/SkySkimmer/bignums notation-uid 20911
5 changes: 3 additions & 2 deletions interp/notation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1268,11 +1268,12 @@ let hashtbl_check_and_set allow_overwrite uid f h eq =
(str "Unique identifier " ++ str uid ++
str " already used to register a number or string (un)interpreter.")

let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
let register_gen_interpretation allow_overwrite (uid:string) (interp, uninterp) : prim_token_uid =
hashtbl_check_and_set
allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
hashtbl_check_and_set
allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq;
uid

let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
register_gen_interpretation allow_overwrite uid
Expand Down
10 changes: 5 additions & 5 deletions interp/notation.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ type rawnum = NumTok.Signed.t
If at most one interpretation of prim token is used per scope,
then the scope name could be used as unique id. *)

type prim_token_uid = string
type prim_token_uid = private string

type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
Expand All @@ -102,13 +102,13 @@ type 'a prim_token_interpretation =
'a prim_token_interpreter * 'a prim_token_uninterpreter

val register_rawnumeral_interpretation :
?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
?allow_overwrite:bool -> string -> rawnum prim_token_interpretation -> prim_token_uid

val register_bignumeral_interpretation :
?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
?allow_overwrite:bool -> string -> Z.t prim_token_interpretation -> prim_token_uid

val register_string_interpretation :
?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
?allow_overwrite:bool -> string -> string prim_token_interpretation -> prim_token_uid

(** * Number notation *)

Expand Down Expand Up @@ -189,7 +189,7 @@ type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj

type prim_token_interp_info =
Uid of prim_token_uid
| Uid of prim_token_uid
| NumberNotation of number_notation_obj
| StringNotation of string_notation_obj

Expand Down
Loading