diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 2545e494ef..1d01d75c82 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -91,19 +91,19 @@ type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter val register_rawnumeral_interpretation : - prim_token_uid -> rawnum prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit val register_string_interpretation : - prim_token_uid -> string prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } |