In the Proofmode tactics and workflow documentation, the focus_block n "Hprog" as a_mid Ha_mid "Hblock" "Hcont" tactic only works given some requirements on the content of the PC resource.
Since these requirements are not mentioned by the error message, it would be useful if the documentation specifies what those requirements are.
In the Proofmode tactics and workflow documentation, the
focus_block n "Hprog" as a_mid Ha_mid "Hblock" "Hcont"tactic only works given some requirements on the content of thePCresource.Since these requirements are not mentioned by the error message, it would be useful if the documentation specifies what those requirements are.