GitLab

Apparently the introduction of more cumulativity triggered a bug in
8.8.1.

This reverts commit 8f3fd83e.

The calls to `vm_change_dep` were put in without properly benchmarking
them. They do not correspond to the original ltac code, which uses just
`change`.

Move back to main CI branch

See merge request FP/iris-coq!176

This saves another few billion instructions.

To avoid redundant `match_goal`s we use the new combinator
`TT.with_goal_prop`.