Enriched and unified syntax for reduction strategies

[herbelin]

In particular, the proposed syntax has:

• pattern selection for all reductions
• support for fine-tuning iota by enabling/disabling specific constructor names
• support for referring to unfolding databases as in coq/ceps#84

Rendered here.