anchor.diff:              let env_lax = {env with lax=true; use_bv_sorts=true} in
               let _, tlhs, _ = env.type_of env_lax tp.lhs in
               let goal_ty = U.mk_eq2 (env.universe_of env_lax tlhs) tlhs tp.lhs tp.rhs in
  -            let goal, ctx_uvar, _ = 
  -              Env.new_implicit_var_aux reason tp.lhs.pos env goal_ty Allow_untyped None 
  +            let goal, ctx_uvar, _ =
  +              Env.new_implicit_var_aux reason tp.lhs.pos env goal_ty Allow_untyped None
               in
  -            let imp = 
  +            let imp =
                 { imp_reason = "";
                   imp_uvar = fst (List.hd ctx_uvar);
                   imp_tm = goal;
  -                imp_range = tp.lhs.pos 
  +                imp_range = tp.lhs.pos
                 }
               in
  -            let sigelt = 
  +            let sigelt =
                 if is_flex tp.lhs
                 then find_user_tac_for_uvar env (flex_uvar_head tp.lhs)
  -              else if is_flex tp.rhs 
  +              else if is_flex tp.rhs
                 then find_user_tac_for_uvar env (flex_uvar_head tp.rhs)
                 else None
               in
  
positive.code:     let solve_goals_with_tac (imps:implicits) (tac:sigelt) =
          let deferred_goals = DeferredImplicits.sort_goals env imps in
          let guard = { g with implicits = imps; deferred_to_tac=[] } in
          let resolve_tac = 
            match tac.sigel with
            | Sig_let (_, [lid]) ->
              let qn = Env.lookup_qname env lid in
  
negative.code:       match deferred with
        | [] -> g
        | _ ->
          let prob_as_implicit (reason, prob)
            : implicit * sigelt =
            match prob with
            | TProb tp when tp.relation=EQ ->
  