Save pattern definitions/missing cases

Fixes #955. Requires a 'make lib_clean'.
Remove some commented out code
Add stack of elaboration context to ElaboratingArg

This is for argument-specific error reflection.
Initial documentation efforts for effects
Remove some commented-out code
Annotate 'Lazy' with reason for laziness

i.e. is it just for evaluation, or is it for codata? This will be useful
for mixed induction/coinduction and allow the productivity checker to be
cleverer.
Merge pull request #989 from david-christiansen/docs

Docs
Merge pull request #991 from jfdm/doc/effects

Initial documentation efforts for effects
Merge remote-tracking branch 'upstream/master' into unifier-context

Conflicts:
	src/Idris/ElabTerm.hs
Add application context to all error messages

This makes it easier to find errors. It will also enable improved error
reflection soon.
Re-enable function arg error reflection

It now uses the same code path as normal error reflection.
Fix test
Merge pull request #990 from david-christiansen/unifier-context

Add more context to unification errors internally
Fix line number on invocation of :e
Support mixed induction/coinduction with Inf type

Update totality checker so that it checks for 'Delay LazyCodata' being
guarded by constructors/lambdas only, allowing mixed
inductive/coinductive definitions.
Change reduction rules for coinductive definitions

Allow reduction in types, but block any reduction immediately under a
Delay. This means coinductive proofs should now be possible, and
coinductive definitions should be runnable at the REPL even if the
produce an infinite stream.
Change guardedness check for new-style coinduction

Now checks that 'Delay LazyCodata' appears constructor guarded for *all*
coinductive definitions, not just mixed inductive/coinductive. Added
stream processor test.
Require content in tactic/proof blocks

Fixes #995
isFnName should look for exact names

Otherwise we might think a local variable is a function when it shadows
a function.

Fixes #993
Make names accessible before building case split

Otherwise the typechecker won't be able to get at the definition we're
building