Add basic elaboration context tracking to unification
Actually track applications in the elaborator wrt unification fails
Track the providence of unification errors

Unification errors can now be wrapped in a constructor specifying what
function was being applied when they were generated, where it was in the
source, and which argument of the function had a problem.
Update CHANGELOG
Use At to hold FCs
Update test for more informative error messages
Temporarily remove function argument error reflection

It needs to be done right, with the new unification info
Temporarily change back to UN to avoid strange errors
Update for new unification error messages
Fix simple application

Don't expect the types to be inferred immediately. If the types of the
arguments are not solved immediately, push their holes to the end of the
hole queue rather than failing with a Can't Infer Type error.

Also fix for linear patterns - don't erase a repeated name in a function
application.
Remember to save deferred definition types in IBC

Partial fix for #955 (still need to save missing case information,
though this is less important)
Save pattern definitions/missing cases

Fixes #955. Requires a 'make lib_clean'.
Docs for decEq
Remove some commented out code
More docstrings
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