idris-lang/Idris-dev — pull request #1130 by jonsterling (2014-04-30 01:02:30+00:00)
Title: Fixes a problem with custom tactics using Intro & Induction

When making applying a custom tactic using `applyTactic`, there were a few problems.

- `Intro` would previously fail with "Unknown Tactic". The problem appears to have been that the argument of `Intro` is *not* a string, but rather the application of a constructor like `UN` or `MN`.
- `Induction` was not possible; I have added a line to `reifyApp` accordingly.

I'm unable to run the tests on my machine for some reason (#1109), so perhaps Travis will tell us whether this works. It does indeed some to solve