anchor.diff:  
   (* .fsti name (optional) * .fst name * .fsti recorded timestamp (optional) * .fst recorded timestamp  *)
   type m_timestamps = list<(option<string> * string * option<time> * time)>
  +type deps_stack_t = list<env_t> // Environments created while typechecking deps
   
   (*
    * type check remaining dependencies and record the timestamps.
  - * m is the current module name, not the module name of the dependency. it's actually a dummy that is pushed on the stack and never used.
  - * it is used for type checking the fragments of the current module, but for dependencies it is a dummy.
  - * adding it as the stack entry needed it.
    * env is the environment in which next dependency should be type checked.
    * the returned timestamps are in the reverse order (i.e. final dependency first), it's the same order as the stack.
    * note that for dependencies, the stack and ts go together (i.e. their sizes are same)
  - * returns the new stack, environment, and timestamps.
  + * returns the new environment, deps stack, and timestamps.
    *)
  -let rec tc_deps (m:modul_t) (stack:stack_t)
  -                (env:env_t) (remaining:list<string>) (ts:m_timestamps)
  -//      : stack<'env,modul_t> * 'env * m_timestamps
  +let rec tc_deps (deps_stack: deps_stack_t) (env: env_t)
  +                (remaining: list<string>) (ts: m_timestamps)
     = match remaining with
  -    | [] -> stack, env, ts
  +    | [] -> env, (deps_stack, ts)
       | _  ->
  -      let stack = (env, m)::stack in
  -      //setting the restore command line options flag true
  -      let env = push_with_kind env (if Options.lax () then LaxCheck else FullCheck) true "typecheck_modul" in
  +      let deps_stack = env :: deps_stack in
  +      let push_kind = if Options.lax () then LaxCheck else FullCheck in
  +      let env = push (set_check_kind env push_kind) "typecheck_modul" in
  +      Options.restore_cmd_line_options false |> ignore;
         let (intf, impl), env, remaining = tc_one_file remaining env in
         let intf_t, impl_t =
           let intf_t =
  
positive.code:   let errors = FStar.Errors.report_all() |> List.map json_of_issue in
    FStar.Errors.clear ();
  
    let st' = { st with repl_stack = stack; repl_ts = ts;
                        repl_line = line; repl_column = column } in
  
    match res with
    | Some (curmod, env, nerrs) when nerrs = 0 && peek_only = false ->
  
negative.code:  * if we find that the dependency at the head of ts does not match that at the head of the newly computed dependency,
   * or that the dependency is stale, we will typecheck that dependency, and everything that comes after that again
   * the stack and timestamps are passed in "last dependency first" order, so we will reverse them before checking
   * returns the new environment, deps stack, and timestamps
   *)
  let update_deps (filename:string) (env:env_t) ((stk, ts): deps_stack_t * m_timestamps)
    : (env_t * (deps_stack_t * m_timestamps)) =
    let is_stale (intf:option<string>) (impl:string) (intf_t:option<time>) (impl_t:time) :bool =
      let impl_mt = get_file_last_modification_time impl in
      (is_before impl_t impl_mt ||
  