Starting Intro pattern

[Villetaneuse]

First (crude) draft to collect first impressions. I will add more text and examples.

[thomas-lamiaux]

https://github.com/tchajed/coq-tricks/blob/master/src/IntroPatterns.v

There is also supposed to be an intro patter for nested sigma [ X].
It enables to write [ a b c d] rather than [a [b [c d]].

[Villetaneuse]

https://github.com/tchajed/coq-tricks/blob/master/src/IntroPatterns.v

There is also supposed to be an intro patter for nested sigma [ X]. It enables to write [ a b c d] rather than [a [b [c d]].

Ok, will test with which associativity it works.

[thomas-lamiaux]

Actually the refman is quite good on the subject and has interesting examples

[thomas-lamiaux]

I suggest writing it in the same style as chaining tactics