anchor.diff:          end
       | None -> true
     in
  -  let rec until_fixpoint (acc: Env.implicits * bool)
  +  let rec until_fixpoint (later_if_univ_constraint:bool)
  +                         (acc: Env.implicits * bool)
                            (implicits:Env.implicits) : Env.implicits =
       let out, changed = acc in
  +    let until_fixpoint = until_fixpoint later_if_univ_constraint in  //for recursive calls
       match implicits with
       | [] ->
         if not changed
  
positive.code:       giveup env msg orig
  
      | UDeferred wl ->
        solve env (defer_lit "" orig wl)
  
  and solve_maybe_uinsts (env:Env.env) (orig:prob) (t1:term) (t2:term) (wl:worklist) : univ_eq_sol =
      let rec aux wl us1 us2 = match us1, us2 with
  
negative.code:            let msg = mklstr (fun () ->
                          BU.format1 "first_order heuristic cannot solve %s; lhs not a quasi-pattern"
                            (prob_to_string env orig)) in
             giveup_or_defer env orig wl Deferred_first_order_heuristic_failed msg
  
          | Some (bs_lhs, t_res_lhs) ->
            if is_app rhs
  