Fix samples to use Type instead of Set
HNF in unification to speed things up
Distinguish parameters and indices internally in data types
This doesn't do anything, yet, but will become important soon!
Some progress on implementation paper revisions
More sane scoping rules for where/type classes
Parameters in the type signature get propagated, indices do not.
So you no longer need to pass parameters explicitly if you need them
in a where clause, and you no longer need to give explicitly typed
helpers in type class instances for types with indices.
Small library tweaks and documentation update
Magic with explanation in impl-paper
Merge pull request #170 from frytvm/master

Fix samples to use Type instead of Set
Merge pull request #173 from raichoo/javascript

javascript: check for keywords as identifiers
Error handling interpreter needs Functor instance (via bishboria)
Merge branch 'master' of github.com:edwinb/Idris-dev
Fix compile warning in ElabDecls
Reorder the monad transformers in the Idris monad to allow completion

Completion of names will require access to the interpreter
state. Unfortunately, the stacking order of the monad transformers didn't
allow this. This has been changed.

As a side effect, when get was used to access the state, it has been
consistently replaced with getIState.
Lots of implementation paper revision
Note on metatheory
Added metatheoretic properties
Add Unify details in impl-paper
Show how tactics are applied in impl-paper
Tinkering with related work
More on related work