diff options
| author | Emilio Jesus Gallego Arias | 2017-02-22 00:23:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-24 14:18:18 +0100 |
| commit | 584a832d4f681d34c7cbdd87d9ceb7a742b39959 (patch) | |
| tree | 1030c2c5a0a3dbfdb2b08773f2ca56ab80cde835 /kernel/type_errors.ml | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[stm] Remove some obsolete vernacs/classification.
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions