diff options
| author | Maxime Dénès | 2015-02-17 18:19:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-02-17 18:19:49 +0100 |
| commit | 2cc7d0be16ce35f7c87fedde0228f08502f0250f (patch) | |
| tree | 7606f301960d4ed8efdbaa4ecf59c82b68a19db0 /lib/errors.ml | |
| parent | 9bc5a2686497ff5e225510383ccce669bfc19bb9 (diff) | |
Remove non-existing Tactic Definition command from index.
Diffstat (limited to 'lib/errors.ml')
0 files changed, 0 insertions, 0 deletions