diff options
| author | Hugo Herbelin | 2016-04-08 21:32:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-15 16:45:52 +0200 |
| commit | 08dbef1f220c3f97ad1baa159b9f0a6913e922b3 (patch) | |
| tree | a1adce3c7b36a8cefb5127cdc95d45fb6100f690 /kernel/type_errors.mli | |
| parent | 3a54bb00dd2420b2710c2f90e1c0c4cf9c267175 (diff) | |
Build stm debugging messages lazily so that they are not silently
computed when not in debugging mode (especially those printing a
command).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions