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
Show latest version
Compare changes
  • Side-by-side
  • Inline

There are no changes yet

No changes between version 1 and version 1