remove debug prints (leftover)
Proof using: call "clear" to remove from sight the vars not selected

As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.

But it is better than nothing I guess.