diff options
| author | Pierre-Marie Pédrot | 2020-05-08 16:29:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 3af3409a8ec23deb3e0d32f00a31363a36f6209b (patch) | |
| tree | 7bcc87fd19a80424dfad1094b935ced9a7079811 /interp/notation.mli | |
| parent | be56f39ecfc0726772cc6930dbc7657348f008e1 (diff) | |
Generalize the interpretation of syntactic notation as reference to their head.
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..cfe3ea12d0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes -> (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> +(** 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 *) |