aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-29 17:05:45 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-29 17:05:45 +0200
commit82a618e8a4945752698a7900c8af7a51091f7b1b (patch)
treed1d0044005573d11830d264c9eb6802aa9e237a2 /Makefile
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 'Makefile')
0 files changed, 0 insertions, 0 deletions