summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
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 25fbe49b..592c8cf5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -159,6 +159,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
Format.fprintf o "(* %s *)@\n" (generated_line filename);
Format.fprintf o "open import Interp_ast@\n";
+ Format.fprintf o "open import Pervasives@\n";
Format.fprintf o "let defs = ";
Pretty_print.pp_lem_defs o defs;
close_output_with_check ext_o