chore: backtick identifiers in do-tactic attribute messages#11844
Open
alok wants to merge 1 commit intoleanprover:masterfrom
Open
chore: backtick identifiers in do-tactic attribute messages#11844alok wants to merge 1 commit intoleanprover:masterfrom
alok wants to merge 1 commit intoleanprover:masterfrom
