Skip to content

Make `inv` and `oinv` work with numbers

Ralf Jung requested to merge ralf/inv-num into master

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)

Merge request reports