From 37f68259ab0a33c3b5b41de70b08422d9bcd3bec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 May 2014 13:42:34 +0200
Subject: Fixing introduction patterns * and ** when used in a branch so that
 they do not introduce beyond what is under control of the branch. See
 test-suite intros.v for an example.

---
 test-suite/success/intros.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 25e0ec2f7e..bb9fc0c50d 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -22,3 +22,9 @@ hnf.
 match goal with [ |- 0 = 0 ] => reflexivity end.
 Abort.
 
+(* Fixing behavior of "*" and "**" in branches, so that they do not
+   introduce more than what the branch expects them to introduce at most *)
+Goal forall n p, n + p = 0.
+intros [|*]; intro p.
+Abort.
+
-- 
cgit v1.2.3