Added 'mrefine' tactic
Like refine, but uses matching instead of unification to resolve implicit
arguments.
All will become clear, I hope :). This is intended for an additional style of
pattern matching (on types) for better explanation of proofs.
Merge branch 'master' of github.com:edwinb/Idris-dev