Add pkg-config gc flags to llvm Makefile

This makes building work for systems which have gc installed in a
non-standard location.  The invocation was pulled from
https://github.com/schani/clojurec/pull/2, and then modified based on
https://github.com/idris-lang/Idris-dev/pull/428#issuecomment-26302460.
Make prover better at IDESlave protocol

Instead of returning strings that comprise results, return actions that
complete them. This makes handling which requests are completed much easier.
Keep type arguments of = when unelaborating

This allows more informative error messages when the mismatch is in the
type arguments to =.
Support multiple let bindings

This sort of thing now works:

  test : Nat -> Nat
  test n = let foo = n
               S k = plus foo foo
              in k

The bindings must be aligned, and the keyword 'in' (indented however you
like within the 'test' block) terminates the list.

Pattern match alternatives are also supported, for quickly catching
failures:

  test2 : Nat -> Nat
  test2 n = let foo = n
                S k = plus foo foo
                    | Z => 42
              in k

Fixes #1362
Remove commented out code
Fix parameter expansion in PEq case
Fix parameter propagation on CAFs

Specifically, only propagate implicit parameters which are missing.
Fixes #1370
Allow :doc in prover

This supports looking up documentation while proving. It's really most
useful inside of an IDE.
Merge pull request #1371 from david-christiansen/prover-output-color

Prover output color
Make type search work in the prover

This patch does two things:

1. It adds support for a new prover command, :search, with the same
syntax and semantics as the REPL command

2. It makes :search work properly with IDESlave, enabling type search
from the Emacs prover as well as enabling length-limits in the IRC bot
again.
Merge pull request #1375 from david-christiansen/type-search-in-prover

Make type search work in the prover
Allow :let in ideslave
Merge pull request #1376 from Melvar/ideslave-let

Allow :let in ideslave
Add Ord instance for Bool
Add parens on generated S patterns

This fixes an issue where generated S patterns would sometimes not be
parenthesized, leading to invalid patterns being generated. This
occurred even in tutorial code, like Parity.
Don't do trace when `with` doesn't match

This breaks IDESlave support. RE #879
Merge pull request #1379 from david-christiansen/paren-S-pat

Add parens on generated S patterns
Merge pull request #1377 from puffnfresh/missing-instances

Add Ord instance for Bool
Merge pull request #1380 from david-christiansen/no-trace-on-with

Get rid of `trace` in error def
Remove dodgy unification hack

Also need to recheck unification problems immediately after setting
injective arguments, or we get strange results for disambiguation.
Fixes #1372