anchor.diff:          let s = [S.NT (bv, S.bv_to_name bv'')] in
           let bvs = List.map (fun b -> { b with sort = SS.subst s b.sort}) bvs in
           let env' = push_bvs e0 (bv''::bvs) in
  -        bind dismiss (fun _ ->
  +        bind __dismiss (fun _ ->
           bind (add_goals [{goal with context = env';
                                       witness = SS.subst s goal.witness;
                                       goal_ty = SS.subst s goal.goal_ty }]) (fun _ ->
  
positive.code: let smt : tac<unit> =
      bind cur_goal (fun g ->
      if is_irrelevant g then
          bind dismiss (fun _ -> add_smt_goals [g])
      else
          fail1 "goal is not irrelevant: cannot dispatch to smt (%s)" (tts g.context g.goal_ty)
      )
  
negative.code:     bind cur_goal (fun g ->
      bind (new_uvar "dup" g.context g.goal_ty) (fun u ->
      let g' = { g with witness = u } in
      bind __dismiss (fun _ ->
      bind (add_irrelevant_goal "dup equation" g.context
                 (U.mk_eq2 (TcTerm.universe_of g.context g.goal_ty) g.goal_ty u g.witness) g.opts) (fun _ ->
      bind (add_goals [g']) (fun _ ->
  