• What can I do when Qed. is slow?
• Conversion not recorded in the proof trace
• An explosion of universes
• The guard checker
• What if Qed is still slow for some reason that is not one of these three?
• Why does Reset Initial. not work when using coqc?
• What can I do if I get "No more subgoals but non-instantiated existential variables"?
• What can I do if I get “Cannot solve a second-order unification problem”?
• I copy-paste a term and Coq says it is not convertible to the original term. Sometimes it even says the copied term is not well-typed.
• What can I do when setoid_rewrite hangs?