Prepare for moving to trunk with some minor workarounds for known changes

These are work-arounds for minor known changes:
- [refine] will now permit dependent goals, so we need to use [eapply]
  to get the same resulting goals
- We need to not clear section variables when the proof depends on them
  (https://coq.inria.fr/bugs/show_bug.cgi?id=3418)
- Higher order unification has changed, so we need to give more things
  explicitly now (https://coq.inria.fr/bugs/show_bug.cgi?id=3269).  In
  particular, Coq had to use a heuristic to decide [f b = ?X b] by
  instantiating [X] to [f], and not e.g. [λ x, f b] ([b] is in [?X]'s
  context).