anchor.diff:               match (SS.compress hd).n with
                | Tm_uvar _ -> true //still unresolved
                | _ -> false) in
  -        solve goal solution;
  +        bind (solve goal solution) (fun _ ->
           bind (add_implicits implicits) (fun _ ->
  -        bind dismiss (fun _ ->
           let is_free_uvar uv t =
               let free_uvars = List.map fst (BU.set_elements (SF.uvars t)) in
               List.existsML (fun u -> UF.equiv u uv) free_uvars
  
positive.code: let trysolve (goal : goal) (solution : term) : bool =
      do_unify goal.context solution goal.witness
  
  let solve (goal : goal) (solution : term) : unit =
      if trysolve goal solution
      then ()
      else raise (TacFailure(BU.format3 "%s does not solve %s : %s"
                            (N.term_to_string goal.context solution)
                            (N.term_to_string goal.context goal.witness)
                            (N.term_to_string goal.context goal.goal_ty)))
  
  let dismiss : tac<unit> =
      bind get (fun p ->
      set ({p with goals=List.tl p.goals}))
  
  let dismiss_all : tac<unit> =
      bind get (fun p ->
  
negative.code:         | Tm_fvar fv, [_; (l, _); (r, _)] when S.fv_eq_lid fv PC.eq2_lid ->
              if not (do_unify g.context l r)
              then fail2 "trefl: not a trivial equality (%s vs %s)" (N.term_to_string g.context l) (N.term_to_string g.context r)
              else solve g U.exp_unit
          | hd, _ ->
              fail1 "trefl: not an equality (%s)" (N.term_to_string g.context t)
          end
  