anchor.diff:                "F* may be in an inconsistent state.\n" ^
                 "Please file a bug report, ideally with a " ^
                 "minimized version of the program that triggered the error." in
  -    FStar.TypeChecker.Err.add_errors env [(msg, TcEnv.get_range env)];
  +    FStar.TypeChecker.Err.add_errors tcenv [(msg, TcEnv.get_range tcenv)];
       // Make sure the user sees the error, even if it happened transiently while
       // running an automatic syntax checker like FlyCheck.
       Util.print_error msg;
       None
   
     | FStar.Errors.Error(msg, r) when not (Options.trace_error ()) ->
  -    FStar.TypeChecker.Err.add_errors env [(msg, r)];
  +    FStar.TypeChecker.Err.add_errors tcenv [(msg, r)];
       None
   
     | FStar.Errors.Err msg when not (Options.trace_error ()) ->
  -    FStar.TypeChecker.Err.add_errors env [(msg, TcEnv.get_range env)];
  +    FStar.TypeChecker.Err.add_errors tcenv [(msg, TcEnv.get_range tcenv)];
       None
   
   let with_captured_errors env f =
  
positive.code:   else with_captured_errors' env f
  
  let check_frag (dsenv, (env:TcEnv.env)) curmod frag =
    with_captured_errors env (fun () ->
      match tc_one_fragment curmod dsenv env frag with
      | Some (m, dsenv, env) ->
        Some (m, (dsenv, env), FStar.Errors.get_err_count())
  
negative.code:   TcEnv.cleanup_interactive env
  
  let with_captured_errors' env f =
    let tcenv = snd env in
    try
      f ()
    with
  