anchor.diff:                         umax_heuristic_ok=false;
                          attempting=[];
                          wl_deferred=[];
  -                       wl_implicits=[];
  -                       wl_solution_types=[]} in  //AR: defer to tac [] here?
  +                       wl_implicits=[]} in
       let tx = UF.new_transaction () in
       match try_solve env wl' with
  -    | Success (_, defer_to_tac, imps, typs) ->
  +    | Success (_, defer_to_tac, imps) ->
         UF.commit tx;
  -      let wl = extend_wl wl defer_to_tac imps typs in
  +      let wl = extend_wl wl defer_to_tac imps in
         solve env wl
       | Failed (p, s) ->
         UF.rollback tx;
  
positive.code:                then giveup env msg prob
                 else fallback()
  
               | Success (_, defer_to_tac, imps, typs) ->
                 UF.commit tx;
                 let guard =
                     U.mk_conj (p_guard base_prob)
                               (p_guard ref_prob |> guard_on_element wl problem x1) in
                 let wl = solve_prob orig (Some guard) [] wl in
                 let wl = {wl with ctr=wl.ctr+1} in
                 let wl = extend_wl wl defer_to_tac imps typs in
                 solve env (attempt [base_prob] wl)
          else fallback()
  
  
negative.code:               |> BU.set_elements
                |> List.for_all (fun uv -> uv.ctx_uvar_should_check = Allow_unresolved) in
              if is_tac then if tm_ok_for_tac tm
                             then until_fixpoint f (out, true) tl        //Move on to the next imp
                             else until_fixpoint f (hd::out, changed) tl  //Move hd to out
              else begin
                //typecheck the solution
                if Env.debug env <| Options.Other "Rel"
                then BU.print5 "Checking uvar %s resolved to %s at type %s, introduce for %s at %s\n"
                                (Print.uvar_to_string ctx_u.ctx_uvar_head)
  