Stream: Coq users

Topic: Disable typeclass search for Check

Ali Caglayan (Aug 05 2020 at 13:33):

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

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: Oct 04 2023 at 19:01 UTC