anchor.diff:  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 solve (goal : goal) (solution : term) : tac<unit> =
  +    if trysolve goal solution
  +    then dismiss
  +    else fail (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_all : tac<unit> =
       bind get (fun p ->
  
positive.code:                     fail2 "exact: term is not typeable: %s (%s)" (Print.term_to_string t) (Print.tag_of_term t)) (fun (t, typ, guard) ->
      if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "exact: got non-trivial guard" else
      if do_unify goal.context typ goal.goal_ty
      then let _ = solve goal t in dismiss
      else fail3 "%s : %s does not exactly solve the goal %s"
                      (N.term_to_string goal.context t)
                      (N.term_to_string goal.context (bnorm goal.context typ))
  
negative.code:              match (SS.compress hd).n with
               | Tm_uvar _ -> true //still unresolved
               | _ -> false) in
          bind (solve goal solution) (fun _ ->
          bind (add_implicits implicits) (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
  