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.
---
 vernac/prettyp.ml       | 4 ++--
 vernac/vernacentries.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

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