From 9c2662eecc398f38be3b6280a8f760cc439bc31c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 01:43:10 +0100
Subject: Stronger invariants on the use of the introduction pattern
 (pat1,...,patn).

The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.

Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
---
 test-suite/success/intros.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index af5f994010..ee69df9774 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -105,3 +105,26 @@ Inductive I := C : let x:=1 in x=1 -> I.
 Goal I -> True.
 intros [x H]. (* Was failing in 8.5 *)
 Abort.
+
+(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
+   to skipping let-ins *)
+
+Goal I -> 1=1.
+intros (H).  (* This skips x *)
+exact H.
+Qed.
+
+Goal I -> 1=1.
+Fail intros (x,H,H').
+Fail intros [|].
+intros (x,H).
+exact H.
+Qed.
+
+Goal Acc le 0 -> True.
+Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
+induction 1 as (n,H,IH).
+exact Logic.I.
+Qed.
+
+
-- 
cgit v1.2.3