diff options
| author | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
| commit | 56e23844e80e6d607ad5fa56dfeedcd70e97ee70 (patch) | |
| tree | 403c7b43e73fa4159fd997ca26953098b34e22b5 /vernac | |
| parent | cc54af3842cbf99f169f7937b0e31f737652bd3a (diff) | |
| parent | b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f (diff) | |
Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime.
Reviewed-by: herbelin
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 6568d7bf14..09201d727d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,7 +1785,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" |