diff options
| author | Jason Gross | 2016-07-05 14:05:07 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-07-05 14:05:07 -0400 |
| commit | f6701cffa04c0df25634ad60004fbfcf4ca422ec (patch) | |
| tree | 48521239fcdee811c8593ab732a837e73e3a3b5f /kernel/nativelambda.ml | |
| parent | d8825650bd2b7855a92195c032a539aa3f09c9ef (diff) | |
Compat84: Don't mess with stdlib modules
We don't actually need to, unless we want to support the (presumably
uncommon) use-case of someone using [Import VectorNotations] to override
their local notation for things in vector_scope.
Additionally, we now maintain the behavior that [Import VectorNotations]
opens vector_scope.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions