diff options
| author | coqbot-app[bot] | 2020-11-16 16:24:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:24:02 +0000 |
| commit | a400dbf104ea3bf0fef51a62e774fb4ff60a7397 (patch) | |
| tree | 296319fab9b42a4ad2c67e879de777996ecc26b5 | |
| parent | 58b24bdf4393d5522df63d31b2adc9eb08c417d8 (diff) | |
| parent | cf4105502388e437c1cf361b5c3ddd8a482eef04 (diff) | |
Merge PR #13212: Suggesting to use injection when an injection pattern is given to destruct (wish #13205)
Reviewed-by: gares
Ack-by: Blaisorblade
Ack-by: RalfJung
| -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: |