Certain tactics, such as mlRewriteBy only work if the goal is using AnyReasoning. However, if they are used with something different, they fail with a useless error message (mlRewriteBy says "not in proof mode"). Instead, they should signal that the ProofInfo is incorrect, or add an extra ProofInfoLE AnyReasoning i goal, like mlApplyMeta does in similar situations.
This limitation is also undocumented.
Certain tactics, such as
mlRewriteByonly work if the goal is usingAnyReasoning. However, if they are used with something different, they fail with a useless error message (mlRewriteBysays "not in proof mode"). Instead, they should signal that theProofInfois incorrect, or add an extraProofInfoLE AnyReasoning igoal, likemlApplyMetadoes in similar situations.This limitation is also undocumented.