diff options
| author | Emilio Jesus Gallego Arias | 2020-02-20 13:56:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-20 13:56:23 -0500 |
| commit | f748ca04748ef00b85de7f31dc1dc7f0a985ec3f (patch) | |
| tree | 60a101df6b546e33878a9ac0900d1009f666c7be /interp/notation.mli | |
| parent | 935101ee1375ed930e993d0e76f2325ade562506 (diff) | |
| parent | a8307ceecc4347593e67cff2044a250b75060f5a (diff) | |
Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index ea5125f7ec..26c45d5896 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool (** Equality on [notation_entry_level]. *) +val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool + val notation_eq : notation -> notation -> bool (** Equality on [notation]. *) module NotationSet : Set.S with type elt = notation module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet +module SpecificNotationSet : Set.S with type elt = specific_notation +module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet (** {6 Scopes } *) (** A scope is a set of interpreters for symbols + optional @@ -213,7 +217,7 @@ val availability_of_prim_token : (** Binds a notation in a given scope to an interpretation *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> @@ -236,7 +240,7 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> subscopes -> +val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option (** {6 Miscellaneous} *) @@ -299,8 +303,8 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -type entry_coercion = notation list -val declare_entry_coercion : notation -> notation_entry_level -> unit +type entry_coercion = (notation_with_optional_scope * notation) list +val declare_entry_coercion : specific_notation -> 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 |