Added span in parser state
Skip unnecessary coverage checking

If the last clause in a definition contains only _, we don't need to
coverage check it. This vastly, vastly improves the speed of this defn:

fourTupleElems : TT -> Maybe (TT, (TT, (TT, TT)))
fourTupleElems (App (App (App (App p ty1) ty2) tm1)
                (App (App (App (App p ty3) ty4) tm2)
                 (App (App (App (App p ty1) ty2) tm3) tm4))) = Just (tm1, tm2, tm3, tm4)
fourTupleElems _ = Nothing
Merge remote-tracking branch 'upstream/master'
Add type signature and Haddock to processTactic'
Upstream updates to idrislang.sty

+ Fixed braces problem.
+ Removed clutter from file.
+ allowed for a static indent for xleftmargin.
Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/parserspanning

Conflicts:
	src/Idris/ParseHelpers.hs
Remove the ability to reflect At and Elaborating

This is because they are primarily "plumbing" for tracking error
locations, so it's better for error reflection to work on their
payloads. Any reasonable implementation would have just copied what the
compiler does with them anyway.
Prepared data structure of FC for spanning, and added the span of the
last token parsed to Idris
Fixed error reflection bug after change of sourcelocation definition
Unification tweak; better disambiguation

Fixes #963. Do alternatives after normal arguments so that more type
information is available.

(Ideally, order shouldn't matter - would be better to retry alternative
resolution if there were still ambiguities at the end, but this will be
fiddly to set up as things currently are.)
Merge pull request #964 from jfdm/idrislang

Upstream updates to idrislang.sty
Merge pull request #965 from ahmadsalim/feature/parserspanning

Preparation for spanning of source code in parser
Fix regression with data declarations in where

Also, start adding tests for examples from the tutorial (we need to
cover it all, really).
Reverse the reversible errors while reflecting

This makes Eff error reflection much more readable.
Add with_val and pureM syntax

Allows updating the set of effects based on a declared return value
(pure is not quite enough for this: we need to provide the return value
then a program which updates the set of effects/states to justify it
being a value return value!)

e.g. (somewhat contived, but...)

  readInt : { [STATE (Vect n Int), STDIO] ==>
              {done} if done then [STATE (Vect n Int), STDIO]
                             else [STATE (Vect (S n) Int), STDIO] }
                             Eff IO Bool
  readInt = do let x = trim !getStr
               if (x == "END")
                  then pureM True
                  else do putM (cast x :: !get)
                          pureM False

pureM x is equivalent to with_val x (pure ())
Improve error pretty-printing
Tail recrusive foldr for List
Tail recursive foldr, reverse and fromList for Vect
Tests for tail recursive implementations of foldr
Make 'neweffects' the official effects package

Old effects is still there if anyone needs it, as 'oldeffects' but this
will be removed later.