We use impredicative-set

[jeehoonkang]

We are using impredicative set, which means that our universe is inconsistent with mathematically well-respected axioms. See on impredicative-set: http://coq.inria.fr/faq (find "impredicative").

Prof. Gil Hur said that vellvm seems not use impredicativity in fundamental way, so we can remove it. It seems once CompCert used it, so maybe the option sneaked in vellvm from CompCert.

So I would like to try to remove impredicative-set option, if possible.