Automatic proof of inequality of datatype constructor with its arguments
Manual rewriter for arithmetic on constants
Overflow of description in tactic profile editor
better type synthesis for datatype
These changes have been merged in commit [df38cb].
More automatic proofs about finiteness
These cases have been implemented and merged in commit [3fc052].
Avoid startup error when external provers timeout