anchor.diff:          else bind (check bvs) (fun () ->
           let env' = push_bvs e' bvs in
           bind (new_uvar "clear.witness" env' goal.goal_ty) (fun ut ->
  -        if do_unify goal.context goal.witness ut
  +        bind (do_unify goal.context goal.witness ut) (fun b ->
  +        if b
           then replace_cur ({ goal with context = env'; witness = ut })
  -        else fail "Cannot clear; binder appears in witness"))))
  +        else fail "Cannot clear; binder appears in witness")))))
   
   let clear_top : tac<unit> =
       bind cur_goal (fun goal ->
  
positive.code:                             (Print.term_to_string t2) in
      try
              let res = Rel.teq_nosmt env t1 t2 in
              debug_off(); res
      with | _ -> debug_off(); false
  
  //    try Rel.teq_nosmt env t1 t2
  //    with | _ -> false
  
  let trysolve (goal : goal) (solution : term) : bool =
      do_unify goal.context solution goal.witness
  
  let dismiss : tac<unit> =
  
negative.code: let set (p:proofstate) : tac<unit> =
      mk_tac (fun _ -> Success ((), p))
  
  let do_unify (env : env) (t1 : term) (t2 : term) : tac<bool> =
      let debug_on () =
          let _ = Options.set_options Options.Set "--debug_level Rel --debug_level RelCheck" in
          ()
  