diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..3480d1c8f2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -211,18 +211,28 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_rule_core = + interp_rule (* kind of notation *) + * interpretation (* pattern associated to the notation *) + * int option (* number of expected arguments *) + +type notation_rule = + notation_rule_core + * delimiters option (* delimiter to possibly add *) + * bool (* true if the delimiter is mandatory *) (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : subscopes -> 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 -> (scope_name option * delimiters option) option + *) (** {6 Miscellaneous} *) @@ -233,6 +243,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool +(** Checks for already existing notations *) +val exists_notation_interpretation_in_scope : scope_name option -> notation -> 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 |