anchor.diff:  let repl_current_qid : ref<option<string>> = Util.mk_ref None // For messages
   let repl_stack: ref<repl_stack_t> = Util.mk_ref []
   
  -let pop_repl st =
  +let pop_repl msg st =
     match !repl_stack with
     | [] -> failwith "Too many pops"
  -  | (depth, (_, st')) :: stack ->
  -    let env = rollback st.repl_env.solver "REPL pop_repl" depth in
  -    repl_stack := stack;
  -    // CPC FIXME if not (Util.physical_equality env st'.repl_env) then failwith "Inconsistent stack state";
  +  | (depth, (_, st')) :: stack_tl ->
  +    let env = rollback_env st.repl_env.solver msg depth in
  +    repl_stack := stack_tl;
  +    // Because of the way ``snapshot`` is implemented, the `st'` and `env`
  +    // that we rollback to should be consistent:
  +    FStar.Common.runtime_assert
  +      (Util.physical_equality env st'.repl_env)
  +      "Inconsistent stack state";
       st'
   
  -let push_repl push_kind task st =
  -  let depth, env = snapshot (set_check_kind st.repl_env push_kind) "REPL push_repl" in
  +let push_repl msg push_kind task st =
  +  let depth, env = snapshot_env st.repl_env msg in
     repl_stack := (depth, (task, st)) :: !repl_stack;
  -  env
  +  { st with repl_env = set_check_kind env push_kind } // repl_env is the only mutable part of st
   
   (** Check whether users can issue further ``pop`` commands. **)
   let nothing_left_to_pop st =
  
positive.code:     curmod, Universal.load_interface_decls env intf.tf_fname
    | PushFragment frag ->
      tc_one_fragment curmod env frag
  
  (** Build a list of dependency loading tasks from a list of dependencies **)
  let repl_ld_tasks_of_deps (deps: list<string>) (final_tasks: list<repl_task>) =
  
negative.code:   | LDInterleaved (_, tf) | LDSingle tf | LDInterfaceOfCurrentFile tf ->
      let modname = Parser.Dep.module_name_of_file tf.tf_fname in
      write_progress (Some "loading-dependency") [("modname", JsonStr modname)]
    | _ -> ()
  
  (** Compute and load all dependencies of `filename`.
  
  