aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-09-29 17:05:45 +0200
committerGuillaume Melquiond2015-09-29 17:05:45 +0200
commit82a618e8a4945752698a7900c8af7a51091f7b1b (patch)
treed1d0044005573d11830d264c9eb6802aa9e237a2 /kernel/nativecode.ml
parentda4d0b0e3d82621fe8338dd313b788472fc31bb2 (diff)
Prevent States.intern_state and System.extern_intern from looking up files in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions