The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Emilio Jesús Gallego Arias 
>>>>> <gallego AT cri.ensmp.fr>
>>>>>  writes:

> I have also found quite useful ssreflect's
>
> "set f := pattern"
>
> tactic to find out types of tricky sub-expressions; the matching mechanism
> usually works well for my full-of-holes patterns.

I would like to second this, and the use of ssreflect in general -- even if
you stick to standard Coq libraries and tactics, it can still be used to
simplify your code with its wonderful rewriting tactic, identification of
subexpressions with set, destructuring "let:", and its improved Search
capability.

After switching all of my code to use ssreflect's libraries and tactics, I
find that many scenarios which were complex or laborious before have become
much simpler to reason about.

John