coq/coq — pull request #40 by JasonGross (2014-10-27 21:23:06+00:00)
Title: Add tactics [test] and [not]

These are generally useful low-level tactics for doing tests in ltac,
which seem like they might be useful in the standard library.

I don't know how they fare with regard to multi-goal tactic invocations,
because I don't know the syntax for that. (There should probably be
backwards compatibility checks in the test-suite, though.)

Are there simpler ways to code these tactics that pass all the tests I
gave? Should these actually be coded in ml?