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] ..].

0 files changed, 0 insertions, 0 deletions