anchor.diff:          bind (add_goals [g1; g2]) (fun _ ->
           ret (S.bv_to_name v_p, S.bv_to_name v_q)))
       | _ ->
  -        fail1 "Not a disjunction: %s" (N.term_to_string g.context typ)))
  +        fail1 "Not a disjunction: %s" (tts g.context typ)))
   
   let set_options (s : string) : tac<unit> =
       bind cur_goal (fun g ->
  
positive.code:         match (U.un_uinst hd).n, args with
          | 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
       | None ->
          fail "not an irrelevant goal")
  
negative.code:     let g_binders = Env.all_binders g.context |> Print.binders_to_string ", " in
      let w = bnorm g.context g.witness in
      let t = bnorm g.context g.goal_ty in
      Util.format3 "%s |- %s : %s" g_binders (tts g.context w) (tts g.context t)
  
  let tacprint  (s:string)       = BU.print1 "TAC>> %s\n" s
  let tacprint1 (s:string) x     = BU.print1 "TAC>> %s\n" (BU.format1 s x)
  