diff options
| author | Pierre-Marie Pédrot | 2020-03-11 11:29:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 245b94cd075b6be527590c425a98262d89577909 (patch) | |
| tree | 0e989e6db3f1e113cc0bb59c92f6e88424f92b79 /kernel/nativelambda.ml | |
| parent | 693c0fb3ad7344aadc840ab7124782e64997b739 (diff) | |
Hack a non-superglobal mode for hints.
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions