Do not load opaque proofs
Simplify some code in Allocate.v
Many code reductions, by using ssreflect better