diff options
| author | Matthieu Sozeau | 2014-10-12 14:38:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 11:43:20 +0200 |
| commit | 6bcb0ebf3552e544db8b3ac8f7d00beaec81059d (patch) | |
| tree | 7144c3f1024b3773b8ce6c58dccb916387f7413a /kernel/nativelib.mli | |
| parent | 4703e70b4086bcc14fdd06b3afd98cad0b45157f (diff) | |
Add an option to not print primitive projection parameters, which can
make printing exponentially slower. We would have to expand all projections
at once before detyping to make this linear.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions