Is it possible to disable typeclass search for the Check
command?
sadly, I only know About
, epose
; commands like notypeclasses refine
exist, if you want that badly enough to try sth like
Goal True. epose (ltac:(notypeclasses refine (your term))).
Last updated: Oct 13 2024 at 01:02 UTC