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.

7 files changed, 30 insertions, 29 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))
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ff1e8b92d1..fcedbe8e2e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -97,7 +97,7 @@ let intern_global_reference ist qid =
   else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
     let id = qualid_basename qid in
     ArgArg (qid.CAst.loc, GlobRef.VarRef id)
-  else match locate_global_with_alias qid with
+  else match locate_global_with_alias ~head:true qid with
   | r -> ArgArg (qid.CAst.loc, r)
   | exception Not_found ->
     if not !strict_check && qualid_is_ident qid then
@@ -315,13 +315,13 @@ let intern_evaluable ist = function
     end
   | {v=ByNotation (ntn,sc);loc} ->
     let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
-    let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in
+    let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
     evalref_of_globref ?loc r
 
 let intern_smart_global ist = function
   | {v=AN r} -> intern_global_reference ist r
   | {v=ByNotation (ntn,sc);loc} ->
-      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
         GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
 
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v
index 1be6d2502a..29b1451822 100644
--- a/theories/Floats/FloatLemmas.v
+++ b/theories/Floats/FloatLemmas.v
@@ -49,7 +49,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
   rewrite Hmod_elim.
   clear Hmod_elim.
   revert Hv.
-  unfold SpecFloat.valid_binary, bounded, canonical_mantissa.
+  unfold valid_binary, bounded, canonical_mantissa.
   unfold fexp.
   rewrite Bool.andb_true_iff.
   intro H'.
@@ -62,7 +62,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
     destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (H, Hm) | (H, Hm) ].
     + rewrite Hm in H1.
       rewrite <- H1.
-      rewrite !Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+      rewrite !Z.max_l by (revert He; unfold emax, emin, prec; lia).
       replace (emin + _)%Z with emax by ring.
       unfold shl_align.
       rewrite <- H1 in H.
@@ -74,7 +74,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold fexp.
       unfold Zdigits2.
       unfold shr_record_of_loc, shr.
-      rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
+      rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
       replace (_ - _)%Z with (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z by ring.
       assert (Hs : (Z.pos (digits2_pos (shift_pos p m)) <= prec)%Z).
       {
@@ -103,26 +103,26 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold round_nearest_even.
       remember (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z as ds.
       destruct ds.
-      * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+      * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
-        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
-        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
         reflexivity.
       * exfalso; lia.
-      * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+      * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
-        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
-        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
         reflexivity.
-    + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
+    + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
       rewrite Hm in H1.
       clear Hm.
       replace (Zpos _ + _ - _)%Z with (e0 + (emax - emin))%Z by (rewrite <- H1 at 1; ring).
@@ -134,7 +134,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold shr_fexp.
       unfold fexp.
       unfold Zdigits2.
-      rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
+      rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
       unfold shr_record_of_loc.
       unfold shr.
       unfold Zdigits2.
@@ -142,17 +142,17 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold shr_m.
       unfold loc_of_shr_record.
       unfold round_nearest_even.
-      rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
+      rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
       replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
-      rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
+      rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
       replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
       reflexivity.
   - rewrite Z.min_le_iff.
     intro H.
-    destruct H as [ He | Habs ]; [ | revert Habs; now unfold SpecFloat.emin, emax ].
+    destruct H as [ He | Habs ]; [ | revert Habs; now unfold emin, emax ].
     unfold shl_align.
     assert (Hprec : (Z.pos (digits2_pos m) <= prec)%Z).
     {
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index a7170c8e18..faf53d3fad 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -906,7 +906,7 @@ let print_name env sigma na udecl =
   match na with
   | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
     print_any_name env sigma
-      (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+      (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
                ntn sc))
       udecl
   | {loc; v=Constrexpr.AN ref} ->
@@ -960,7 +960,7 @@ let print_about env sigma na udecl =
   match na with
   | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
       print_about_any ?loc env sigma
-        (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+        (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
                ntn sc)) udecl
   | {loc;v=Constrexpr.AN ref} ->
       print_about_any ?loc env sigma (locate_any_name ref) udecl
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aac0b54ed4..b8dce9ed44 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1779,7 +1779,7 @@ let interp_search_about_item env sigma =
       try
         let ref =
           Notation.interp_notation_as_global_reference
-            (fun _ -> true) s sc in
+            ~head:false (fun _ -> true) s sc in
         GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
         user_err ~hdr:"interp_search_about_item"