Non-strict proof-mode allows SMT failures to be catchable with try and affiliated. This tends to lead to hardly maintainable proofs and is not used anymore.
The commits remove the internal handling of non-strict proof scripts, removing the proof strict / proof -strict syntax.
The only leftover is the try! tactical that allows to catch SMT failures. It is useful for debugging purpose but should not remain in final scripts.
Non-strict proof-mode allows SMT failures to be catchable with
tryand affiliated. This tends to lead to hardly maintainable proofs and is not used anymore.The commits remove the internal handling of non-strict proof scripts, removing the
proof strict/proof -strictsyntax.The only leftover is the
try!tactical that allows to catch SMT failures. It is useful for debugging purpose but should not remain in final scripts.