summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-09-13 15:12:28 +0100
committerBrian Campbell2018-09-13 15:12:45 +0100
commit61abeccf6c37169bc22a1674897caf482195857f (patch)
treeec7c94584b50f9af3ccc27148953f291ad4e0ea6 /src/process_file.ml
parent3bbda62cb341cc7277fc8c70685ad7d9313e2412 (diff)
Coq: real built-ins for AArch64
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 f3fe2dfa..2dfd9571 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -327,6 +327,7 @@ let output_coq filename libs defs =
"Sail2_instr_kinds";
"Sail2_values";
"Sail2_string";
+ "Sail2_real";
operators_module
] @ monad_modules
in