diff --git a/backend/cn/main.ml b/backend/cn/main.ml
index 4156a4ec2..ba9baebdb 100644
--- a/backend/cn/main.ml
+++ b/backend/cn/main.ml
@@ -56,7 +56,7 @@ open Log
 
 
 
-let frontend incl_dirs astprints filename state_file =
+let frontend incl_dirs incl_files astprints filename state_file =
   let open CF in
   Cerb_global.set_cerb_conf "Cn" false Random false Basic false false false false;
   (* FIXME: make this a global config thing rather than poking state. *)
@@ -65,7 +65,8 @@ let frontend incl_dirs astprints filename state_file =
   Switches.set ["inner_arg_temps"];
   let@ stdlib = load_core_stdlib () in
   let@ impl = load_core_impl stdlib impl_name in
-  let@ (_, ail_prog_opt, prog0) = c_frontend ~cnnames:cn_builtin_fun_names (conf incl_dirs astprints, io) (stdlib, impl) ~filename in
+  let conf = Setup.conf incl_dirs incl_files astprints in
+  let@ (_, ail_prog_opt, prog0) = c_frontend ~cnnames:cn_builtin_fun_names (conf, io) (stdlib, impl) ~filename in
   let markers_env, (_, ail_prog) = Option.get ail_prog_opt in
   Tags.set_tagDefs prog0.Core.tagDefs;
   let prog1 = Remove_unspecs.rewrite_file prog0 in
@@ -100,6 +101,7 @@ let check_input_file filename =
 let main 
       filename 
       incl_dirs
+      incl_files
       loc_pp 
       debug_level 
       print_level 
@@ -137,7 +139,7 @@ let main
   check_input_file filename;
   let (prog4, (markers_env, ail_prog), statement_locs) = 
     handle_frontend_error 
-      (frontend incl_dirs astprints filename state_file)
+      (frontend incl_dirs incl_files astprints filename state_file)
   in
   Cerb_debug.maybe_open_csv_timing_file ();
   Pp.maybe_open_times_channel 
@@ -203,12 +205,17 @@ let file =
   Arg.(required & pos ~rev:true 0 (some string) None & info [] ~docv:"FILE" ~doc)
 
 
-let incl_dir =
+let incl_dirs =
   let doc = "Add the specified directory to the search path for the\
              C preprocessor." in
   Arg.(value & opt_all string [] & info ["I"; "include-directory"]
          ~docv:"DIR" ~doc)
 
+let incl_files =
+  let doc = "Adds  an  implicit  #include into the predefines buffer which is \
+             read before the source file is preprocessed." in
+  Arg.(value & opt_all string [] & info ["include"] ~doc)
+
 let loc_pp =
   let doc = "Print pointer values as hexadecimal or as decimal values (hex | dec)" in
   Arg.(value & opt (enum ["hex", Pp.Hex; "dec", Pp.Dec]) !Pp.loc_pp &
@@ -291,7 +298,8 @@ let () =
   let check_t = 
     const main $ 
       file $ 
-      incl_dir $
+      incl_dirs $
+      incl_files $
       loc_pp $ 
       debug_level $ 
       print_level $
diff --git a/backend/cn/setup.ml b/backend/cn/setup.ml
index 9ac4e8d34..2f388a828 100644
--- a/backend/cn/setup.ml
+++ b/backend/cn/setup.ml
@@ -35,7 +35,7 @@ let io =
 let impl_name = "gcc_4.9.0_x86_64-apple-darwin10.8.0"
 
 (* adapting code from backend/driver/main.ml *)
-let cpp_str incl_dirs =
+let cpp_str incl_dirs incl_files =
   String.concat " " 
     (["cc -std=c11 -E -CC -Werror -nostdinc -undef -D__cerb__";
       "-I " ^ Cerb_runtime.in_runtime "libc/include";
@@ -44,8 +44,10 @@ let cpp_str incl_dirs =
      ]
      @
        List.map (fun str -> "-I " ^ str) incl_dirs
+     @ List.map (fun str -> "-include " ^ str) incl_files
      @
        [" -DDEBUG -DCN_MODE";]
+
     )
 
 let with_cn_keywords str =
@@ -68,7 +70,7 @@ let with_cn_keywords str =
   ) str cn_keywords
 
 
-let conf incl_dirs astprints = 
+let conf incl_dirs incl_files astprints = 
   { debug_level = 0
   ; pprints = []
   ; astprints = astprints
@@ -76,6 +78,6 @@ let conf incl_dirs astprints =
   ; typecheck_core = true
   ; rewrite_core = true
   ; sequentialise_core = true
-  ; cpp_cmd = with_cn_keywords (cpp_str incl_dirs)
+  ; cpp_cmd = with_cn_keywords (cpp_str incl_dirs incl_files)
   ; cpp_stderr = true
   }