diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-13 19:38:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
| commit | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (patch) | |
| tree | 21bda11bb7526d8dccc8c3883245ecf02762fc74 /library/global.mli | |
| parent | 575da16f72ac125ba7e50b1bfe63302dee639973 (diff) | |
Print the type-in-type flag in various user-facing functions.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions