diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 17355dfd..dfc97246 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -833,6 +833,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Printf.fprintf out "Require Import Primitives.\n"; Printf.fprintf out "Import Primitives.\n"; Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n"; + Printf.fprintf out "Require Import List.\n"; + Printf.fprintf out "Import ListNotations.\n"; Printf.fprintf out "Local Open Scope Primitives_scope.\n"; (* Add the custom imports *) |