From a1be9ce30ed0c59d3cd8651ff0c624a24a6d3fc9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Sep 2014 09:50:07 +0200
Subject: Seeing IntroWildcard as an action intro pattern rather than as a
 naming pattern (the action is "clear").

Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.

Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
---
 test-suite/success/intros.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index bb9fc0c50d..9443d01e3b 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -28,3 +28,8 @@ Goal forall n p, n + p = 0.
 intros [|*]; intro p.
 Abort.
 
+(* Check non-interference of "_" with name generation *)
+Goal True -> True -> True.
+intros _ ?.
+exact H.
+Qed.
-- 
cgit v1.2.3