diff options
| author | Arnaud Spiwack | 2014-07-30 14:40:46 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | 96d1dc433019b0f962b823c8d83fb82cdad18c88 (patch) | |
| tree | ad277a5269d8890ab878de0745ec4cbb26512a0e /kernel/type_errors.mli | |
| parent | 78692ad28ded4f94d5cf7e54240fe0b71d1be282 (diff) | |
Add [guard] tactic.
The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails.
Together with [numgoal] can be used to fork on the number of goals of a tactic.
The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions