std++ collides with `Equations`: both define `simplify_eq`, and we mess up their obligation tactic
The equations package seems to also contain a simplify_eq
tactic
Ltac Equations.Init.simplify_eq
Ltac Coq.Init.Ltac.simplify_eq (shorter name to refer to it in current context is Ltac.simplify_eq)
stdpp's simplify_eq
is a notation, and the Coq.Init
version seems to not be a problem, but when equations is imported, the tactic stops working. Instead one gets an obscure error, just saying "Not a negated primitive equality."
This is when equations is imported after std++. When I import equations first, it behaves in strange ways -- there's a different number of obligations generated and they also look different. I think equations might not like our Global Obligation Tactic := idtac.
.