2.5.0

CHANGES:

Added

• Add the opaque command to turn a defined symbol into a constant
• Add the tactic try that tries to apply a tactic to the focused goal.
  If the application of the tactic fails, it catches the error and leaves the goal unchanged.

Fixed

• Coq export: do not rename module names
• Sequential symbols: fix order of rules