anchor.diff:              | None -> "_"
               | Some t -> tts (goal_env g) t
           in
  +        let num = match maybe_num with
  +                  | None -> ""
  +                  | Some (i, n) -> BU.format2 " %s/%s" (string_of_int i) (string_of_int n)
  +        in
           let maybe_label =
               match g.label with
               | "" -> ""
  -            | l -> "Label: " ^ l ^ "\n"
  +            | l -> " (" ^ l ^ ")"
           in
  -        BU.format4 "%s%s |- %s : %s"
  +        BU.format6 "%s%s%s:\n%s |- %s : %s\n\n"
  +             kind
  +             num
                maybe_label
                (Print.binders_to_string ", " g.goal_ctx_uvar.ctx_uvar_binders)
                w
  
positive.code:          | None -> ""
           | Some t -> BU.format1 "\tGOAL ALREADY SOLVED!: %s" (Print.term_to_string t))
  
  let goal_to_string ps (g:goal) =
      if Options.print_implicits ()
         || ps.tac_verb_dbg
      then goal_to_string_verbose g
  
negative.code:     // should somehow taint the state instead of just printing a warning
      Err.log_issue (goal_type g).pos
          (Errors.Warning_TacAdmit, BU.format1 "Tactics admitted goal <%s>\n\n"
                      (goal_to_string "" None ps g));
      solve' g t))
  
  let fresh () : tac<Z.t> =
  