chore: backtick identifiers in elaborator tactic messages#11840
Open
alok wants to merge 2 commits intoleanprover:masterfrom
Open
chore: backtick identifiers in elaborator tactic messages#11840alok wants to merge 2 commits intoleanprover:masterfrom
alok wants to merge 2 commits intoleanprover:masterfrom
Commits
Commits on Dec 30, 2025
Commits on Jan 1, 2026
- andcommitted
