Add `*` versions of `o` tactics.
Failed
Robbert Krebbers
created pipeline for commit
42940f5a
, finished
Related merge request !512 to merge ralf/odestruct
10 minutes 16 seconds, queued for 45 seconds