avoid polymorphic equality; do not export ring_conv (which is not a conversion anyway); renamed algebra_tac to ring_tac; ring_tac: simplified tactic wrapper, no longer handles ERROR;