Refactor parsing of Pi/Dependent Type Signature expressions to improve
error reporting and reduce lookahead.
Restored "__pi_arg" to use UN instead of MN again (due to a test
failure).
Removed commented out code.
Fix erasure from data constructors.
Add a check for missed newtype optimisations.
Fix indentation.
Add Data.Erased to libs/base.
Add workaround for some non-trivial case-matches on detaggable data.
Add a regression test.
Remove trailing whitespace.
Fixes a problem with custom tactics using Intro & Induction

Intro would previously fail with "Unknown Tactic".
Merge pull request #1105 from ahmadsalim/improvement/refactorpis

Improvement/refactorpis
Merge pull request #1106 from ziman/fix-dctor-erasure

Fix erasure from data constructors
Merge pull request #1107 from ziman/data-erased

Add Data.Erased to libs/base
Merge pull request #1112 from PhilipRasmussen/idrisdoc

IdrisDoc cleanups and Haddock additions
Tweak mergeNotunified

No need to add a problem if already equal
Makes rndFin take all values in Fin (S k)

Previously, rndFin k only took values in 0, 1, ... , k - 1, even
though the type Fin (S k) has elements 0, 1, ..., k.
Remove whitespace for :addproof - like :load does

This should probably happen for all commands which take a filename.
Fix addition and subtraction of Complex Float.
Adds docstrings
Adds rndSelect

Adds functions to select random elements from lists and vectors.
These functions also demonstrate the naturalness of the new definition
of rndFin.