anchor.diff:          CTable.register_module_path table (loaded mod_key) mod_path ns_query)
       table (List.rev mods) // List.rev to process files in order or *increasing* precedence
   
  +(** Typecheck prims.fst then compute and typecheck all dependencies of `filename`.
  +
  +If any of these steps fail, rollback the changes (so that calling this function
  +again is safe) and return the resulting environment (wrapped in ``Inr``).  If
  +all steps succeed, return a list of computed dependencies, a dependencies stack
  +(``deps_stack_t``), and the new environment (all wrapped in ``Inr``). **)
  +
   let tc_prims_and_deps env filename =
  -  let _, dsenv, tcenv = tc_prims env in
  -  let deps, maybe_inferface = deps_of_our_file filename in
  -  let env, repl_deps = tc_deps [] (dsenv, tcenv) deps [] in
  -  let env = match maybe_inferface with
  -    | None -> env
  -    | Some intf ->
  -      // We found an interface: record its contents in the desugaring environment
  -      // to be interleaved with the module implementation on-demand
  -      FStar.Universal.load_interface_decls env intf in
  -  (deps, repl_deps, env)
  +  match push_then_do_or_revert_all env [] (fun env -> Some <| tc_prims env) with
  +  | Inr env -> Inr env
  +  | Inl (stack, (_, dsenv, tcenv)) ->
  +    let env = dsenv, tcenv in
  +    match push_then_do_or_revert_all env stack
  +            (fun _env -> Some <| deps_of_our_file filename) with
  +    | Inr env -> Inr env
  +    | Inl (stack, (deps, maybe_interface)) ->
  +      match tc_deps env stack deps with
  +      | Inr env -> Inr env
  +      | Inl (stack, env, ts) ->
  +        match maybe_interface with
  +        | None -> Inl (deps, (stack, ts), env)
  +        | Some intf ->
  +          // We found an interface: record its contents in the desugaring environment
  +          // to be interleaved with the module implementation on-demand
  +          match push_then_do_or_revert_all env stack
  +                  (fun env -> Some <| FStar.Universal.load_interface_decls env intf) with
  +          | Inr env -> Inr env
  +          | Inl (stack, env) -> Inl (deps, (stack, ts), env)
   
   let rephrase_dependency_error issue =
     { issue with issue_message =
  
positive.code: 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.
   * 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 environment, deps stack, and timestamps.
   *)
  let rec tc_deps (deps_stack: deps_stack_t) (env: env_t)
                  (remaining: list<string>) (ts: m_timestamps)
    = match remaining with
      | [] -> env, (deps_stack, ts)
      | _  ->
        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 =
            match intf with
              | Some intf -> Some (get_file_last_modification_time intf)
              | None      -> None
          in
          let impl_t = get_file_last_modification_time impl in
          intf_t, impl_t
        in
        tc_deps deps_stack env remaining ((intf, impl, intf_t, impl_t)::ts)
  
  (*
   * check if some dependencies have been modified, added, or deleted
   * if so, only type check them and anything that follows, while maintaining others as is (current dependency graph is a total order)
  
negative.code:     None
  
  let with_captured_errors env f =
    if Options.trace_error () then f env
    else with_captured_errors' env f
  
  let check_frag (dsenv, tcenv) curmod frag =
    with_captured_errors (dsenv, tcenv) (fun (dsenv, tcenv) ->
      match tc_one_fragment curmod dsenv tcenv frag with
      | Some (m, dsenv, env) ->
        Some (m, (dsenv, env), FStar.Errors.get_err_count())
      | _ -> None)
  