Stream: Coq users

Topic: Debug long Qed or Defined

view this post on Zulip Patrick Nicodemus (Oct 30 2022 at 17:31):

Sometimes when you end a proof it takes Coq a long time to process the tactic script and actually create the term. How does one debug this when it takes a very long time for Qed or Defined to execute?
Similarly in Program mode it can sometimes take Program a very long time to process the Next Obligation command, does anyone have a suggestion for how I might track down why it is so time consuming?

view this post on Zulip Michael Soegtrop (Oct 31 2022 at 08:51):

There are several longer discussions on this here, e.g. (

Last updated: Feb 08 2023 at 23:03 UTC