Make `inv` and `oinv` work with numbers

I also replaced all inversion_clear by inv. In list.v I furthermore replaced most inversion by inv just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleared.

Fixes #199 (closed)

This is great.

However sometimes, follow-up automation fails when the inverted hypothesis is cleared.

Do you have an example? Is that a "feature" or a "bug" of the follow-up automation?

added 1 commit

• 8f2b6c1a - factor out helper tactic for 'run on n-th hypothesis in the goal'

Compare with previous version

added 2 commits

• 61298cb1 - Fix uses of legacy `inversion` in `list.
• c49005ee - Replace all uses of `inversion` by `inv`.

Compare with previous version

resolved all threads

With a CHANGELOG this should be good to go.

added 1 commit

• aa87822c - changelog

Compare with previous version

I extended the existing changelog entry for inv, is that okay?

added 5 commits

• f0ba256f - make 'oinv 1' work
• 1223a173 - factor out helper tactic for 'run on n-th hypothesis in the goal'
• b6c59a7d - Fix uses of legacy `inversion` in `list.
• 33f33107 - Replace all uses of `inversion` by `inv`.
• 2afec065 - changelog

Compare with previous version

resolved all threads

merged

mentioned in commit 8c98553a

Merging. Thanks for the work.