Top Answers

1. Is it possible to turn unification errors into goals in Coq?
   5 votes
2. Weird goal `Some 0 = true` generated in proof
   3 votes
3. Removing trivial match clause in Coq
   2 votes