diff options
| author | Hugo Herbelin | 2020-10-16 22:15:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 15:45:36 +0100 |
| commit | cf4105502388e437c1cf361b5c3ddd8a482eef04 (patch) | |
| tree | 4ac4a1ad1c52b6ae793ba762c350edca3c7b0df7 | |
| parent | fb186f25abeb0565bb6e238345f0c5147b697322 (diff) | |
Suggesting to use injection when an injection pattern is given to destruct.
This hopefully clarifies the confusing role of destruct (see #13205).
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index ecfe6c1664..236de65462 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -450,6 +450,11 @@ GRAMMAR EXTEND Gram ; as_or_and_ipat: [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat } + | "as"; ipat = equality_intropattern -> + { match ipat with + | IntroRewrite _ -> user_err Pp.(str "Disjunctive/conjunctive pattern expected.") + | IntroInjection _ -> user_err Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.") + | _ -> assert false } | -> { None } ] ] ; eqn_ipat: |