diff options
| author | Emilio Jesus Gallego Arias | 2017-03-30 14:58:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:49:46 +0200 |
| commit | cf24cedb2926fa00db222eeac48e88a6078b4444 (patch) | |
| tree | 649354ba1da3c3747f1e30c1a6d1f32dd5b2b470 /kernel/term_typing.ml | |
| parent | 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 (diff) | |
[stm] [nit] Centralize compile-time debug flag.
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions