diff options
| author | Pierre-Marie Pédrot | 2020-05-08 16:29:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 3af3409a8ec23deb3e0d32f00a31363a36f6209b (patch) | |
| tree | 7bcc87fd19a80424dfad1094b935ced9a7079811 /vernac | |
| parent | be56f39ecfc0726772cc6930dbc7657348f008e1 (diff) | |
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.
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" |