anchor.diff:  
   
   let store_module_to_cache env fn (m:modul) (modul_iface_opt:option<modul>) (mii:DsEnv.module_inclusion_info) =
  -    let cache_file = FStar.Parser.Dep.cache_file_name fn in
  -    let digest = FStar.Parser.Dep.hash_dependences env.dep_graph fn in
  -    match digest with
  -    | Some hashes ->
  -      //cache_version_number should always be the first field here
  -      BU.save_value_to_file cache_file (cache_version_number, hashes, m, modul_iface_opt, mii)
  -    | _ ->
  -      FStar.Errors.log_issue
  -        (FStar.Range.mk_range fn (FStar.Range.mk_pos 0 0)
  -                                 (FStar.Range.mk_pos 0 0))
  -        (Errors.Warning_FileNotWritten, BU.format1 "%s was not written, since some of its dependences were not also checked"
  -                    cache_file)
  +    if Options.cache_checked_modules() then
  +        let cache_file = FStar.Parser.Dep.cache_file_name fn in
  +        let digest = FStar.Parser.Dep.hash_dependences env.dep_graph fn in
  +        match digest with
  +        | Some hashes ->
  +          //cache_version_number should always be the first field here
  +          BU.save_value_to_file cache_file (cache_version_number, hashes, m, modul_iface_opt, mii)
  +        | _ ->
  +          FStar.Errors.log_issue
  +            (FStar.Range.mk_range fn (FStar.Range.mk_pos 0 0)
  +                                     (FStar.Range.mk_pos 0 0))
  +            (Errors.Warning_FileNotWritten, BU.format1 "%s was not written, since some of its dependences were not also checked"
  +                        cache_file)
   
   (***********************************************************************)
   (* Batch mode: checking a file                                         *)
  
positive.code:     in
      fun env fn ->
          let cache_file = Dep.cache_file_name fn in
          let fail tag =
               invalidate_cache();
               FStar.Errors.log_issue
                  (Range.mk_range fn (Range.mk_pos 0 0) (Range.mk_pos 0 0))
                  (Errors.Warning_CachedFile, BU.format3 "%s cache file %s; will recheck %s and all subsequent files" tag cache_file fn);
               None
          in
          match !some_cache_invalid with
  
negative.code:       let mii = FStar.Syntax.DsEnv.inclusion_info env.dsenv (fst tcmod).name in
        tcmod, tcmod_iface_opt, mii, env
    in
    match load_module_from_cache env fn with
    | None ->
          let tcmod, tcmod_iface_opt, mii, env = tc_source_file () in
          if FStar.Errors.get_err_count() = 0
          && (Options.lax()  //we'll write out a .checked.lax file
              || Options.should_verify (fst tcmod).name.str) //we'll write out a .checked file
          //but we will not write out a .checked file for an unverified dependence
          //of some file that should be checked
          then store_module_to_cache env fn (fst tcmod) tcmod_iface_opt mii;
          tcmod, env, None
    | Some (tcmod, tcmod_iface_opt, mii) ->
          let tcmod =
          if tcmod.is_interface then tcmod
          else
              let use_interface_from_the_cache = Options.use_extracted_interfaces () && pre_fn = None &&
                                              (not (Options.expose_interfaces ()  && Options.should_verify tcmod.name.str)) in
              if use_interface_from_the_cache then
              if tcmod_iface_opt = None then
              begin
                  FStar.Errors.log_issue (Range.mk_range tcmod.name.str
                                                      (Range.mk_pos 0 0)
                                                      (Range.mk_pos 0 0))
                                      (Errors.Warning_MissingInterfaceOrImplementation,
                                          "use_extracted_interfaces option is set \
                                          but could not find an interface in the cache for: "
                                          ^ tcmod.name.str);
                  tcmod
              end
              else tcmod_iface_opt |> must
              else tcmod
          in
          let delta_env env =
              let _, env =
              with_tcenv env <|
              FStar.ToSyntax.ToSyntax.add_modul_to_env tcmod mii (FStar.TypeChecker.Normalize.erase_universes env)
              in
              FStar.TypeChecker.Tc.load_checked_module env tcmod
          in
          (tcmod,0), env, extend_delta_env delta delta_env
  
  (***********************************************************************)
  (* Batch mode: composing many files in the presence of pre-modules     *)
  