diff options
| author | Gaëtan Gilbert | 2020-07-03 15:15:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-03 15:15:20 +0200 |
| commit | cf388fdb679adb88a7e8b3122f65377552d2fb94 (patch) | |
| tree | b852fd1e116ff72748210a11bc95298453ac2e4d /interp/notation.mli | |
| parent | 33581635d3ad525e1d5c2fb2587be345a7e77009 (diff) | |
| parent | 53e19f76624b7a18792af799e970e9478f8e90a9 (diff) | |
Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in custom gr…
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index e7e917463b..c39bfa6e28 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -298,8 +298,8 @@ type symbol = val symbol_eq : symbol -> symbol -> bool (** Make/decompose a notation of the form "_ U _" *) -val make_notation_key : notation_entry_level -> symbol list -> notation -val decompose_notation_key : notation -> notation_entry_level * symbol list +val make_notation_key : notation_entry -> symbol list -> notation +val decompose_notation_key : notation -> notation_entry * symbol list (** Decompose a notation of the form "a 'U' b" *) val decompose_raw_notation : string -> symbol list @@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t +val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level + type entry_coercion = (notation_with_optional_scope * notation) list -val declare_entry_coercion : specific_notation -> notation_entry_level -> unit +val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option val declare_custom_entry_has_global : string -> int -> unit @@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool +(** Dealing with precedences *) + +type level = notation_entry * entry_level * entry_relative_level list + (* first argument is InCustomEntry s for custom entries *) + +val level_eq : level -> level -> bool +val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool + +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) + +val declare_notation_level : notation -> level -> unit +val level_of_notation : notation -> level + (** raise [Not_found] if not declared *) + (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b |