diff --git a/src/3d/Batch.fsti b/src/3d/Batch.fsti
index 1c42b943c..2a04cf7a3 100644
--- a/src/3d/Batch.fsti
+++ b/src/3d/Batch.fsti
@@ -34,6 +34,13 @@ val copy_clang_format
   (out_dir: string)
 : ML unit
 
+val copy_everparse_h
+  (clang_format: bool)
+  (clang_format_executable: string)
+  (_: input_stream_binding_t)
+  (out_dir: string)
+: ML unit
+
 val produce_and_postprocess_one_c
   (_: input_stream_binding_t)
   (emit_output_types_defs: bool)
diff --git a/src/3d/GenMakefile.fst b/src/3d/GenMakefile.fst
index 521a7dde1..6f6f72ea6 100644
--- a/src/3d/GenMakefile.fst
+++ b/src/3d/GenMakefile.fst
@@ -22,6 +22,7 @@ let oext = function
 
 let print_make_rule
   mtype
+  everparse_h
   input_stream_binding
   (r: rule_t)
 : Tot string
@@ -34,17 +35,23 @@ let print_make_rule
       match r.ty with
       | EverParse -> Printf.sprintf "$(EVERPARSE_CMD) --odir %s" output_dir
       | CC ->
-        let iopt = match mtype with
-        | HashingOptions.MakefileGMake -> "-I"
-        | HashingOptions.MakefileNMake -> "/I"
+        let inc =
+          if everparse_h
+          then ""
+          else
+            let iopt = match mtype with
+            | HashingOptions.MakefileGMake -> "-I"
+            | HashingOptions.MakefileNMake -> "/I"
+            in
+            let ddd_home = "$(EVERPARSE_HOME)" `OS.concat` "src" `OS.concat` "3d" in
+            let ddd_actions_home = ddd_home `OS.concat` "prelude" `OS.concat` (HashingOptions.string_of_input_stream_binding input_stream_binding) in
+            Printf.sprintf "%s %s %s %s" iopt ddd_home iopt ddd_actions_home
         in
         let copt = match mtype with
         | HashingOptions.MakefileGMake -> "-c"
         | HashingOptions.MakefileNMake -> "/c"
-        in        
-        let ddd_home = "$(EVERPARSE_HOME)" `OS.concat` "src" `OS.concat` "3d" in
-        let ddd_actions_home = ddd_home `OS.concat` "prelude" `OS.concat` (HashingOptions.string_of_input_stream_binding input_stream_binding) in
-        Printf.sprintf "$(CC) $(CFLAGS) %s %s %s %s %s" iopt ddd_home iopt ddd_actions_home copt
+        in
+        Printf.sprintf "$(CC) $(CFLAGS) %s %s" inc copt
     in
     let rule = Printf.sprintf "%s\t%s %s\n\n" rule cmd r.args in
     rule
@@ -432,6 +439,7 @@ let produce_output_types_o_rule
     
 let produce_o_rule
   mtype
+  (everparse_h: bool)
   (modul: string)
 : Tot rule_t
 =
@@ -439,13 +447,14 @@ let produce_o_rule
   let o = mk_filename modul (oext mtype) in
   {
     ty = CC;
-    from = [c; mk_filename modul "h"];
+    from = ((if everparse_h then [mk_filename "EverParse" "h"] else []) `List.Tot.append` [c; mk_filename modul "h"]);
     to = o;
     args = c_to_o mtype o c;
   }
 
 let produce_wrapper_o_rule
   mtype
+  (everparse_h: bool)
   (g: Deps.dep_graph)
   (modul: string)
 : Tot (list rule_t)
@@ -457,7 +466,7 @@ let produce_wrapper_o_rule
   if Deps.has_entrypoint g modul
   then [{
     ty = CC;
-    from = [wc; wh; h];
+    from =((if everparse_h then [mk_filename "EverParse" "h"] else []) `List.Tot.append` [wc; wh; h]);
     to = wo;
     args = c_to_o mtype wo wc;
   }]
@@ -465,6 +474,7 @@ let produce_wrapper_o_rule
 
 let produce_static_assertions_o_rule
   mtype
+  (everparse_h: bool)
   (g: Deps.dep_graph)
   (modul: string)
 : Tot (list rule_t)
@@ -475,7 +485,7 @@ let produce_static_assertions_o_rule
   if Deps.has_static_assertions g modul
   then [{
     ty = CC;
-    from = [wc; h];
+    from = ((if everparse_h then [mk_filename "EverParse" "h"] else []) `List.Tot.append` [wc; h]);
     to = wo;
     args = c_to_o mtype wo wc;
   }]
@@ -493,6 +503,26 @@ let produce_clang_format_rule
    args = "--__micro_step copy_clang_format";
   }] else []
 
+let produce_everparse_h_rule
+  (everparse_h: bool)
+: Tot (list rule_t)
+=
+  if everparse_h
+  then [
+    {
+      ty = EverParse;
+      from = [];
+      to = mk_filename "EverParseEndianness" "h";
+      args = "--__micro_step copy_everparse_h";
+    };
+    {
+      ty = Nop;
+      from = [mk_filename "EverParseEndianness" "h"];
+      to = mk_filename "EverParse" "h";
+      args = "";
+    }
+  ] else []
+
 noeq
 type produce_makefile_res = {
   rules: list rule_t;
@@ -502,6 +532,7 @@ type produce_makefile_res = {
 
 let produce_makefile
   mtype
+  (everparse_h: bool)
   (emit_output_types_defs: bool)
   (skip_o_rules: bool)
   (clang_format: bool)
@@ -512,12 +543,13 @@ let produce_makefile
   let all_files = Deps.collect_and_sort_dependencies_from_graph g files in
   let all_modules = List.map Options.get_module_name all_files in
   let rules =
+    produce_everparse_h_rule everparse_h `List.Tot.append`
     produce_clang_format_rule clang_format `List.Tot.append`
     (if skip_o_rules then [] else
-      List.Tot.concatMap (produce_wrapper_o_rule mtype g) all_modules `List.Tot.append`
-      List.Tot.concatMap (produce_static_assertions_o_rule mtype g) all_modules `List.Tot.append`
+      List.Tot.concatMap (produce_wrapper_o_rule mtype everparse_h g) all_modules `List.Tot.append`
+      List.Tot.concatMap (produce_static_assertions_o_rule mtype everparse_h g) all_modules `List.Tot.append`
       List.concatMap (produce_output_types_o_rule mtype emit_output_types_defs g) all_modules `List.Tot.append`
-      List.Tot.map (produce_o_rule mtype) all_modules
+      List.Tot.map (produce_o_rule mtype everparse_h) all_modules
     ) `List.Tot.append`
     List.concatMap (produce_fst_rules emit_output_types_defs g clang_format) all_files `List.Tot.append`
     List.concatMap (produce_external_types_fsti_checked_rule g) all_modules `List.Tot.append`
@@ -538,6 +570,7 @@ let produce_makefile
 let write_makefile
   mtype
   input_stream_binding
+  (everparse_h: bool)
   (emit_output_types_defs: bool)
   (skip_o_rules: bool)
   (clang_format: bool)
@@ -546,10 +579,14 @@ let write_makefile
 =
   let makefile = Options.get_makefile_name () in
   let file = FStar.IO.open_write_file makefile in
-  let {graph = g; rules; all_files} = produce_makefile mtype emit_output_types_defs skip_o_rules clang_format files in
-  FStar.IO.write_string file (String.concat "" (List.Tot.map (print_make_rule mtype input_stream_binding) rules));
+  let {graph = g; rules; all_files} = produce_makefile mtype everparse_h emit_output_types_defs skip_o_rules clang_format files in
+  FStar.IO.write_string file (String.concat "" (List.Tot.map (print_make_rule mtype everparse_h input_stream_binding) rules));
   let write_all_ext_files (ext_cap: string) (ext: string) : FStar.All.ML unit =
     let ln =
+      begin if ext = "h" && everparse_h
+      then [mk_filename "EverParse" "h"; mk_filename "EverParseEndianness" "h"]
+      else []
+      end `List.Tot.append`
       begin if ext <> "h"
       then
         List.concatMap (fun f -> let m = Options.get_module_name f in if Deps.has_static_assertions g m then [mk_filename (Printf.sprintf "%sStaticAssertions" m) ext] else []) all_files
diff --git a/src/3d/GenMakefile.fsti b/src/3d/GenMakefile.fsti
index e2a46a86d..d10641d25 100644
--- a/src/3d/GenMakefile.fsti
+++ b/src/3d/GenMakefile.fsti
@@ -3,6 +3,7 @@ module GenMakefile
 val write_makefile
   (mtype: HashingOptions.makefile_type)
   (_: HashingOptions.input_stream_binding_t)
+  (everparse_h: bool)
   (emit_output_types_defs: bool)
   (skip_o_rules: bool)
   (clang_format: bool)
diff --git a/src/3d/HashingOptions.fst b/src/3d/HashingOptions.fst
index 8618d1d06..44a845c61 100644
--- a/src/3d/HashingOptions.fst
+++ b/src/3d/HashingOptions.fst
@@ -11,6 +11,7 @@ type micro_step_t =
   | MicroStepVerify
   | MicroStepExtract
   | MicroStepCopyClangFormat
+  | MicroStepCopyEverParseH
   | MicroStepEmitConfig
   
 type makefile_type =
diff --git a/src/3d/Main.fst b/src/3d/Main.fst
index e8341b8e5..50887b6bc 100644
--- a/src/3d/Main.fst
+++ b/src/3d/Main.fst
@@ -601,6 +601,17 @@ let go () : ML unit =
     let _ = Batch.copy_clang_format (Options.get_output_dir ()) in
     exit 0
   else
+  if micro_step = Some HashingOptions.MicroStepCopyEverParseH
+  then
+  (* Special mode: --__micro_step copy_everparse_h *)
+    let _ = Batch.copy_everparse_h
+      (Options.get_clang_format ())
+      (Options.get_clang_format_executable ())
+      (Options.get_input_stream_binding ())
+      (Options.get_output_dir ())
+    in
+    exit 0
+  else
   (* for other modes, a nonempty list of files is needed on the command line, so if none are there, then we shall print the help message *)
   let input_stream_binding = Options.get_input_stream_binding () in
   if Nil? cmd_line_files
@@ -622,6 +633,7 @@ let go () : ML unit =
     GenMakefile.write_makefile
       t
       input_stream_binding
+      (not (Options.get_no_everparse_h ()))
       (Options.get_emit_output_types_defs ())
       (Options.get_skip_o_rules ())
       (Options.get_clang_format ())
diff --git a/src/3d/Options.fst b/src/3d/Options.fst
index bdda1bcc7..ea94e3243 100644
--- a/src/3d/Options.fst
+++ b/src/3d/Options.fst
@@ -67,6 +67,7 @@ let valid_micro_step (str: string) : Tot bool = match str with
   | "verify"
   | "extract"
   | "copy_clang_format"
+  | "copy_everparse_h"
   | "emit_config"
     -> true
   | _ -> false
@@ -389,7 +390,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
     CmdOption "z3_test_mode" (OptStringOption "pos|neg|all" valid_z3_test_mode z3_test_mode) "produce positive, negative, or all kinds of test cases (default all)" [];
     CmdOption "z3_witnesses" (OptStringOption "nb" always_valid z3_witnesses) "ask for nb distinct test witnesses per branch case (default 1)" [];
     CmdOption "__arg0" (OptStringOption "executable name" always_valid arg0) "executable name to use for the help message" [];
-    CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|emit_config" valid_micro_step micro_step) "micro step" [];
+    CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|copy_everparse_h|emit_config" valid_micro_step micro_step) "micro step" [];
     CmdOption "__produce_c_from_existing_krml" (OptBool produce_c_from_existing_krml) "produce C from .krml files" [];
     CmdOption "__skip_deps" (OptBool skip_deps) "skip dependency analysis, assume all dependencies are specified on the command line" [];
   ];
@@ -484,6 +485,7 @@ let get_micro_step _ =
   | Some "verify" -> Some MicroStepVerify
   | Some "extract" -> Some MicroStepExtract
   | Some "copy_clang_format" -> Some MicroStepCopyClangFormat
+  | Some "copy_everparse_h" -> Some MicroStepCopyEverParseH
   | Some "emit_config" -> Some MicroStepEmitConfig
 
 let get_produce_c_from_existing_krml _ =
diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml
index 42a7e6dd6..0a0a8115e 100644
--- a/src/3d/ocaml/Batch.ml
+++ b/src/3d/ocaml/Batch.ml
@@ -604,6 +604,24 @@ let add_copyright
   
 (* Call clang-format *)
 
+let call_clang_format_on
+  (clang_format_executable: string)
+  (files: string list)
+= match files with
+  | [] -> ()
+  | _ ->
+  let clang_format_args =
+    "-i" ::
+      "--style=file" ::
+        files
+  in
+  let clang_format_exe =
+    if clang_format_executable <> ""
+    then clang_format_executable
+    else Printf.sprintf "clang-format%s" (if Sys.win32 then ".exe" else "")
+  in
+  run_cmd clang_format_exe clang_format_args
+
 let call_clang_format
       (no_everparse_h: bool)
       (produced_files: bool)
@@ -612,21 +630,8 @@ let call_clang_format
       (out_dir: string)
       (files_and_modules: (string * string) list)
   =
-  let clang_format_exe =
-    if clang_format_exe0 <> ""
-    then clang_format_exe0
-    else Printf.sprintf "clang-format%s" (if Sys.win32 then ".exe" else "")
-  in
   let files = collect_files no_everparse_h produced_files wrappers out_dir files_and_modules in
-  match files with
-  | [] -> ()
-  | _ ->
-  let clang_format_args =
-    "-i" ::
-      "--style=file" ::
-        files
-  in
-  run_cmd clang_format_exe clang_format_args
+  call_clang_format_on clang_format_exe0 files
 
 (* Check and Save hashes *)
 
@@ -705,6 +710,26 @@ let save_hashes
 let copy_clang_format out_dir =
   copy (filename_concat ddd_home ".clang-format") (filename_concat out_dir ".clang-format")
 
+let copy_everparse_h_raw
+      input_stream_binding
+      out_dir =
+      let dest_everparse_h = filename_concat out_dir "EverParse.h" in
+      let everparse_h_source = (filename_concat (ddd_actions_c_home input_stream_binding) "EverParse.h") in
+      if file_exists everparse_h_source
+      then copy everparse_h_source dest_everparse_h;
+      let everparse_endianness_source = (filename_concat ddd_home (Printf.sprintf "EverParseEndianness%s.h" (if Sys.win32 then "_Windows_NT" else ""))) in
+      if file_exists everparse_endianness_source
+      then copy everparse_endianness_source (filename_concat out_dir "EverParseEndianness.h")
+
+let copy_everparse_h
+      (clang_format: bool)
+      (clang_format_executable: string)
+      input_stream_binding
+      out_dir =
+  copy_everparse_h_raw input_stream_binding out_dir;
+  if clang_format
+  then call_clang_format_on clang_format_executable [filename_concat out_dir "EverParse.h"; filename_concat out_dir "EverParseEndianness.h"]
+
 (* Postprocess C files, assuming that they have already been processed *)
 
 let postprocess_c
@@ -725,13 +750,7 @@ let postprocess_c
   (* copy EverParse.h unless prevented *)
   if not no_everparse_h
   then begin
-      let dest_everparse_h = filename_concat out_dir "EverParse.h" in
-      let everparse_h_source = (filename_concat (ddd_actions_c_home input_stream_binding) "EverParse.h") in
-      if file_exists everparse_h_source
-      then copy everparse_h_source dest_everparse_h;
-      let everparse_endianness_source = (filename_concat ddd_home (Printf.sprintf "EverParseEndianness%s.h" (if Sys.win32 then "_Windows_NT" else ""))) in
-      if file_exists everparse_endianness_source
-      then copy everparse_endianness_source (filename_concat out_dir "EverParseEndianness.h")
+      copy_everparse_h_raw input_stream_binding out_dir
     end;
   (* clang-format the files if asked for *)
   if clang_format