Skip to content

Commit

Permalink
fix: use throwUnknownConstant
Browse files Browse the repository at this point in the history
  • Loading branch information
fgdorais committed Dec 22, 2024
1 parent ea23c55 commit c76e44a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Batteries/Tactic/PrintOpaques.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ partial def collect (c : Name) : M Unit := do
unless ← Meta.isProp v.type do
modify fun s => { s with opaques := s.opaques.push c }
| none =>
panic! s!"unknown constant {c}"
throwUnknownConstant c

end CollectOpaques

Expand Down

0 comments on commit c76e44a

Please sign in to comment.