Removing tactic compatibility layer in Equality.
Removing Tacmach compatibility layer in Equality.
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.