This allows for tactics like recover and classical that have been transformed from regular tactics into block tactics to be able to capture the list of subsequent tactics into the block. (We can't use Mathport.Syntax.Transform for this because it's not an adjacent tactic transformation. It's also a mandatory transformation - the result is not well formed if the transformation is not applied - unlike most syntax transforms which are optional.)
This allows for tactics like
recoverandclassicalthat have been transformed from regular tactics into block tactics to be able to capture the list of subsequent tactics into the block. (We can't useMathport.Syntax.Transformfor this because it's not an adjacent tactic transformation. It's also a mandatory transformation - the result is not well formed if the transformation is not applied - unlike most syntax transforms which are optional.)