Correct opening brace in implicits in pprinter

Before:
    Prelude.Basics.id : (a : Type} -> (__pi_arg : a) -> a

After:
    Prelude.Basics.id : {a : Type} -> (__pi_arg : a) -> a
--link and --include give flags, not directories
Add check after each proof step, not just the end

In elaboration, unification errors aren't always fatal, because some
information may turn up later which fixes things. Interactive proofs
ought to have immediate feedback instead.
Fixes #974

It may also be worth considering automatically filling more things in by
unification (refine currently requires each explicit argument to be
given explicitly, because that is easier to explain). Possibly this
should be a different tactic.
Merge pull request #1097 from david-christiansen/pprint

Correct opening brace in implicits in pprinter
Merge pull request #1103 from PhilipRasmussen/idrisdoc

IdrisDoc tests + bug fix
Merge pull request #1104 from puffnfresh/docs

--link and --include give flags, not directories
trans doesn't need homogeneous equalities
Add 'unify' tactic

Normally, we give every explicit argument to a function after 'refine',
even if some may be solvable by unification. The 'unify' tactic goes
back and fills in the unifiable ones.

(I don't expect this to be useful *that* often but I have occasionally
encountered such situations.)
Merge 'not unified' variables

That is, explicitly given variables which could otherwise be unified. If
they appear several times in the notunified list, make sure they all
match.

Fixes #1077
Better error for ambiguous instance name

Fixes #1066
Fixed typo
IdrisDoc now merges documentation more robustly using less code.