package coq-libhyps

This library defines a set of tactics to manipulate hypothesis individually or by group. In particular it allows applying a tactic on each hypothesis of a goal, or only on new hypothesis after some tactic. Examples of manipulations: automatic renaming, subst, revert, or any tactic expecting a hypothesis name as argument.

It DOES NOT provide ANYMORE the especialize tactic to ease forward reasoning by instantianting one, several or all premisses of a hypothesis. Ths is due to coq's specialize being less permissive about evars. This may be fixed in the future.