Minor changes to unerase tactic to cope with Coq bugs about Section Variables.

Also update gaptreebfacts with hybrid non-findings.