diff options
| author | coqbot-app[bot] | 2020-10-12 12:53:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-12 12:53:02 +0000 |
| commit | a78b394d372f259107017cdb129be3fe53a15894 (patch) | |
| tree | eef0043d55f2ec739b48906f4b16b9b61d162e41 /interp/notation.mli | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
| parent | 3e32cf5b791cb5653520f68cd3d2677733b32324 (diff) | |
Merge PR #12950: Notations: reworking the treatment of only-parsing and only-printing notations
Reviewed-by: SkySkimmer
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 948831b317..d744ff41d9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -229,12 +229,24 @@ type interp_rule = | NotationRule of specific_notation | SynDefRule of KerName.t -val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> - Deprecation.t option -> unit +type notation_use = + | OnlyPrinting + | OnlyParsing + | ParsingAndPrinting val declare_uninterpretation : interp_rule -> interpretation -> unit +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +val declare_notation : notation_with_optional_scope * notation -> + interpretation -> notation_location -> use:notation_use -> + entry_coercion_kind option -> + Deprecation.t option -> unit + + (** Return the interpretation bound to a notation *) val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) @@ -257,16 +269,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option +val is_printing_inactive_rule : interp_rule -> interpretation -> bool + (** {6 Miscellaneous} *) (** If head is true, also allows applied global references. *) val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t -(** Checks for already existing notations *) -val exists_notation_in_scope : scope_name option -> notation -> - bool -> interpretation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit |