This way, it won't pick arbitrary (and possibly wrong!) inG instances
when multiple ones are available. We achieve this by declaring:

  Hint Mode inG - - +

So that type class inference only succeeds when the type of the ghost
variable does not include any evars.

This required me to make some minor changes throughout the whole
development making some types explicit.

This reverts commit c43eb936.

The hack using class_apply has some strange behaviors, see:

  https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html

Also, I removed the @ from lookup_weaken since the Coq bug we
experienced before somehow disappeared.

Also, add algebra/gset to _CoqProject.

There was not really a need for the lattice type classes, so I removed
these.