From f0ff590f380fb3d9fac6ebfdd6cfd7bf6874658e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Nov 2015 18:43:07 +0100
Subject: Updating test-suite after Bracketing Last Introduction Pattern set by
 default. Interestingly, there is an example where it makes the rest of the
 proof less natural.

Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].

where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.

Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":

intros [|p1|p1]; [intros y|intros [|p2|p2] ..].
---
 test-suite/output/Cases.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5ebc2..a95b085ac0 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -73,7 +73,7 @@ Definition f : B -> True.
 
 Proof.
 intros [].
-destruct b as [|] ; intros _ ; exact Logic.I.
+destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
-- 
cgit v1.2.3