diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 3 insertions, 3 deletions
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" |