summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorpes202019-08-20 10:05:40 +0100
committerpes202019-08-20 10:05:40 +0100
commiteedb8aa907cd6b89d0ce5978129124346f084b99 (patch)
tree3ee2e7fa409293ddd2a9f9fbfd81003eaf96b841 /src/process_file.ml
parent9942726dfab4d7b32d910b8365e40d8178331084 (diff)
add -coq_alt_modules option to override the default imported modules
Diffstat (limited to 'src/process_file.ml')
0 files changed, 0 insertions, 0 deletions