diff options
| author | Gaëtan Gilbert | 2019-01-04 09:12:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-04 09:12:03 +0100 |
| commit | 246012c65aff12bae347be57b0432128a593c72a (patch) | |
| tree | 294616dc2236ec38fae84e0a3b173bd3d694ef50 /kernel/type_errors.ml | |
| parent | 0a5bbf347b5bbcb579f94eb3d0166778cd92cfdb (diff) | |
Default disable auto template warning.
The situation is too unclear to make it of general use, plus it has
some issues (#9296)
I'm not deleting the warning as it can still be useful to find which
types are template for those who want to experiment.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions