package rocq-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 also provides the especialize tactic to ease forward reasoning by instantianting one, several or all premisses of a hypothesis.