From cf4105502388e437c1cf361b5c3ddd8a482eef04 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 16 Oct 2020 22:15:03 +0200
Subject: Suggesting to use injection when an injection pattern is given to
 destruct.

This hopefully clarifies the confusing role of destruct (see #13205).
---
 plugins/ltac/g_tactic.mlg | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

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:
-- 
cgit v1.2.3