Skip to content

Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`

Robbert Krebbers requested to merge robbert/eunify into master

Merge request reports

Loading