summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-08-10 18:37:24 +0100
committerBrian Campbell2018-08-10 18:37:51 +0100
commit3f2205e552d850c5eb128f4763ea0e4016e43ad2 (patch)
treef68b3d1a6a74611e2f3fb9b564f9237b342f1f6c /src/process_file.ml
parentc0a1b055e093e4c2d6ada52abb01a7abfff40794 (diff)
Coq: add some of string library
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 958720ea..96029587 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -309,6 +309,7 @@ let output_coq filename libs defs =
let base_imports = [
"Sail2_instr_kinds";
"Sail2_values";
+ "Sail2_string";
operators_module
] @ monad_modules
in