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

added 3 commits

• fb3f1a9d - Add `eunify` tactic.
• aaaa20d7 - Test cases for `eunify`.
• 7630a598 - Add CHANGELOG.

Compare with previous version

As an alternative to defining a new tactic, we could shadow Coq's existing unify tactic. Not sure if that's preferred or not.

@jung I need this tactic for some of the f_equiv and f_contractive changes that we talked about.

Yes please! I mean really Coq's unify should take open_constr already, but this is better than nothing. I recall running against this wall some time last year.

added 3 commits

• ddfd5b06 - Add `eunify` tactic.
• f6a91817 - Test cases for `eunify`.
• eca37705 - CHANGELOG.

Compare with previous version

resolved all threads

merged

mentioned in commit e377efdf