Add hsenv directory to gitignore
Pattern variables should be lifted to top level

...since pattern variables scope across the whole expression. If we
don't lift them, mysterious unification errors can happen for implicit
arguments.
Fix typo in comment
Don't build Idris twice in CI

This is a pretty decent speedup. :) We need cabal register so idris-llvm
can find the Idris library to link against. Otherwise cabal will
helpfully resolve the dependency by downloading Idris from Hackage for
us.
A new primitive tactic for getting source locations

The tactic sourceLocation fills the hole with the current location in
the file. If such information is unavailable, it fails.

This is to be used by DSL implementers to provide useful error
messages that can't be caught at type-check time. Additionally, it may
prove useful for debugging and assertion libraries, so they can report
errors.

Because the tactic merely fills out an implicit argument in a particular
way, it doesn't break referential transparency, at least not of the core
language. This is similar to the technique used in Scala Virtualized.
Add something like Haskell's "error" function.

It is in Debug.Error.  It prints the source location that it was called
from and a user-supplied message before terminating the program.

Fixes #1692.
Merge pull request #1752 from enolan/master

Don't build Idris twice in CI
Merge pull request #1753 from david-christiansen/feature/source-location-tactic

A new primitive tactic for getting source locations
Merge pull request #1704 from eamsden/master

Add hsenv directory to gitignore
Fix a few typos in the README

[skip ci]
Improve delaboration and pretty-printing for case

Now, the delaborator finds case expressions and converts them back to
the original. This makes :printdef work with these.
Follow instructions in comment and remove unused code
Fix Curses whitespace issue with test delab001
Merge pull request #1758 from david-christiansen/feature/case-delab

Improve delaboration and pretty-printing for "case"
Merge pull request #1756 from jonatack/patch-1

Fix a few typos in the README
Improvement for 'auto'

Now proof search can be deferred if there are too many metavariables in
the goal - previously in this case it would happily pick any old
solution causing weird errors elsewhere in some cases.