Stream: Coq users

Topic: Disable typeclass search for Check

view this post on Zulip Ali Caglayan (Aug 05 2020 at 13:33):

Is it possible to disable typeclass search for the Check command?

view this post on Zulip Paolo Giarrusso (Aug 05 2020 at 13:57):

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: Jun 15 2024 at 05:01 UTC