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.

3 files changed, 10 insertions, 9 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 7761606f11..47cf4ec6ef 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1807,10 +1807,10 @@ let browse_notation strict ntn map =
       map [] in
   List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
 
-let global_reference_of_notation test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
   match c with
   | NRef ref when test ref -> Some (ntn,sc,ref)
-  | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
+  | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
       Some (ntn,sc,ref)
   | _ -> None
 
@@ -1822,14 +1822,14 @@ let error_notation_not_reference ?loc ntn =
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference ?loc test ntn sc =
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
   let scopes = match sc with
   | Some sc ->
       let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
-  let refs = List.map (global_reference_of_notation test) ntns in
+  let refs = List.map (global_reference_of_notation ~head test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
   | [] -> error_notation_not_reference ?loc ntn
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 *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 98fa71e15d..03977fcb4e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -62,15 +62,15 @@ let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
   with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-    global_with_alias ?head r
+    global_with_alias ~head r
   | ByNotation (ntn,sc) ->
-    Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
+    Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
 
 let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_inductive_with_alias r
   | ByNotation (ntn,sc) ->
     destIndRef
-      (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
+      (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))