anchor.diff:  
   let solve (goal : goal) (solution : term) : tac<unit> =
       let e = goal_env goal in
  -    mlog (fun () -> BU.print2 "solve %s := %s\n" (tts e (goal_witness goal)) (tts e solution)) (fun () ->
  +    mlog (fun () -> BU.print2 "solve %s := %s\n" (Print.term_to_string (goal_witness goal))
  +                                                 (Print.term_to_string solution)) (fun () ->
       bind (trysolve goal solution) (fun b ->
       if b
       then bind __dismiss (fun () -> remove_solved_goals)
  
positive.code:                | g::_ -> g.opts
                 | _ -> FStar.Options.peek ()
      in
      mlog (fun () -> BU.print1 "norm_term_env: t = %s\n" (tts ps.main_context t)) (fun () ->
      bind (__tc e t) (fun (t, _, _) ->
      let steps = [N.Reify; N.UnfoldTac]@(N.tr_norm_steps s) in
      let t = normalize steps ps.main_context t in
  
negative.code:         let w =
              match get_uvar_solved g.goal_ctx_uvar with
              | None -> "_"
              | Some t -> tts (goal_env g) t
          in
          BU.format3 "%s |- %s : %s"
               (Print.binders_to_string ", " g.goal_ctx_uvar.ctx_uvar_binders)
               w
               (tts (goal_env g) g.goal_ctx_uvar.ctx_uvar_typ)
  
  let tacprint  (s:string)       = BU.print1 "TAC>> %s\n" s
  let tacprint1 (s:string) x     = BU.print1 "TAC>> %s\n" (BU.format1 s x)
  