Merged requested to merge robbert/decision_true_false_cost into master
This fixes issue #165 (closed).
What happens is that it needs to solve
Decision (@elem_of ... ?instance x xs) where
?instance is an evar representing an unresolved type class. Now instead of solving
?instance first, Coq applies
False_dec and uses HO-unification to instantiate
λ _ _, False, i.e., something nonsensical.
By increasing the cost of the
False instances we make sure Coq first uses the