anchor.diff:    (*
      * When do we keep the body of the letbinding in the interface ...
      *)
  -  let should_keep_lbdef (en:env) (t:typ) :bool =
  +  let should_keep_lbdef (t:typ) :bool =
       let comp_effect_name (c:comp) :lident = //internal function, caller makes sure c is a Comp case
         match c.n with | Comp c -> c.effect_name | _ -> failwith "Impossible!"
       in 
  
positive.code: and finish_partial_modul (loading_from_cache:bool) (en:env) (m:modul) (exports:list<sigelt>) :(modul * option<modul> * env) =
    //AR: do we ever call finish_partial_modul for current buffer in the interactive mode?
    if (not loading_from_cache) && Options.use_extracted_interfaces () && not m.is_interface then begin //if we are using extracted interfaces and this is not already an interface
      //pop AND use the old env for rest of the function
      let en0 = pop_context en ("Ending modul " ^ m.name.str) in
  
      (* extract interface block *)
      //push new context for extracting the interface
      let en0 = push_context en0 ("Extracting interface for " ^ m.name.str) in
      let modul_iface = extract_interface en0 m in
      if Env.debug en <| Options.Low then
        BU.print4 "Extracting and type checking module %s interface%s%s%s\n" m.name.str
                  (if Options.should_verify m.name.str then "" else " (in lax mode) ")
                  (if Options.dump_module m.name.str then ("\nfrom: " ^ (Syntax.Print.modul_to_string m) ^ "\n") else "")
                  (if Options.dump_module m.name.str then ("\nto: " ^ (Syntax.Print.modul_to_string modul_iface) ^ "\n") else "");
      let en0 = pop_context en0 ("Ending interface extraction for " ^ m.name.str) in 
      (* end extract interface block *)
  
      //set up the environment to verify the extracted interface
      let en0 =
        //for hints, we want to use the same id counter as was used in typechecking the module itself, so use the tbl from env
        let en0 = { en0 with qtbl_name_and_index = en.qtbl_name_and_index |> fst, None } in
        if not (Options.interactive ()) then begin  //we should not have this case actually since extracted interfaces are not supported in ide yet
          Options.restore_cmd_line_options true |> ignore;
          z3_reset_options en0
  
negative.code:     in
  
      let modul_iface, must_be_none, env = tc_modul en0 modul_iface in
      if must_be_none <> None then failwith "Impossible! finish_partial_module: expected the second component to be None"
      else { m with exports = modul_iface.exports }, Some modul_iface, env  //note: setting the exports for m, once extracted_interfaces is default, exports should just go away
    end
    else
  