From 3af3409a8ec23deb3e0d32f00a31363a36f6209b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 May 2020 16:29:30 +0200
Subject: 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.
---
 interp/notation.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp/notation.mli')

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 *)
-- 
cgit v1.2.3