Add tactic to solve decidable goals
It is surprisingly hard to find out how to solve a goal exploiting the fact that it is decidable:
apply (bool_decide_unpack _); by compute
IMO it would be a good idea to make that into a tactic. As usual the hardest part is figuring out how to call it. Or alternatively we could make
done also do this, at which point the name basically would not matter.