Skip to content
Snippets Groups Projects

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

Merged Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`
robbert/eunify into master
All threads resolved!
Merged Robbert Krebbers requested to merge robbert/eunify into master
All threads resolved!
Compare
and
Compare changes
  • Side-by-side
  • Inline
Files
4