Rename `simplify_eq` to avoid shadowing Coq's tactic, or document it
Coq has its own simplify_eq
tactic (not a very useful one). And @jung wrote in #73 (closed):
Then the tactic should be renamed to avoid confusion for people that are familiar with the Coq tactic.
That'd suggest renaming std++'s simplify_eq
. In fact, that seems pretty annoying, so maybe we should just prepend a comment to the definition:
(** Unrelated to Coq's own [simplify_eq]. *)