anchor.diff:          else let env' = Env.push_binders goal.context [b] in
                let typ' = comp_to_typ c in
                bind (new_uvar "intro" env' typ') (fun u ->
  -             if trysolve goal (U.abs [b] u None)
  +             bind (trysolve goal (U.abs [b] u None)) (fun bb ->
  +             if bb
                then bind (replace_cur ({ goal with context = env';
                                                    goal_ty = bnorm env' typ';
                                                    witness = bnorm env' u})) (fun _ ->
                     ret b)
                else fail "unification failed"
  -             )
  +             ))
       | None ->
           fail1 "goal is not an arrow (%s)" (tts goal.context goal.goal_ty)
       )
  
positive.code:           ) (fun _ ->
      mlog (fun () -> BU.print2 "exact: unifying %s and %s\n" (tts goal.context typ)
                                                              (tts goal.context goal.goal_ty)) (fun _ ->
      if do_unify goal.context typ goal.goal_ty
      then solve goal t
      else fail4 "%s : %s does not exactly solve the goal %s (witness = %s)"
                      (tts goal.context t)
                      (tts goal.context typ)
                      (tts goal.context goal.goal_ty)
                      (tts goal.context goal.witness)))))
  
  let t_exact set_expected_typ force_guard tm : tac<unit> = wrap_err "exact" <|
      mlog (fun () -> BU.print1 "t_exact: tm = %s\n" (Print.term_to_string tm)) (fun _ ->
  
negative.code:         let hd, args = U.head_and_args' t in
          match (U.un_uinst hd).n, args with
          | Tm_fvar fv, [_; (l, _); (r, _)] when S.fv_eq_lid fv PC.eq2_lid ->
              bind (do_unify g.context l r) (fun b ->
              if not b
              then fail2 "trefl: not a trivial equality (%s vs %s)" (tts g.context l) (tts g.context r)
              else solve g U.exp_unit)
          | hd, _ ->
              fail1 "trefl: not an equality (%s)" (tts g.context t)
          end
  