anchor.diff:            ) (fun _ ->
       mlog (fun () -> BU.print2 "exact: unifying %s and %s\n" (tts goal.context typ)
                                                               (tts goal.context goal.goal_ty)) (fun _ ->
  -    if do_unify goal.context typ goal.goal_ty
  +    bind (do_unify goal.context typ goal.goal_ty) (fun b -> if b
       then solve goal t
       else fail4 "%s : %s does not exactly solve the goal %s (witness = %s)"
                       (tts goal.context t)
                       (tts goal.context typ)
                       (tts goal.context goal.goal_ty)
  -                    (tts goal.context goal.witness)))))
  +                    (tts goal.context goal.witness))))))
   
   let t_exact set_expected_typ force_guard tm : tac<unit> = wrap_err "exact" <|
       mlog (fun () -> BU.print1 "t_exact: tm = %s\n" (Print.term_to_string tm)) (fun _ ->
  
positive.code:     in
      // Lemma post is thunked, and is specialized to U_zero
      let post = U.mk_app post [S.as_arg U.exp_unit] in
      if not (do_unify goal.context (U.mk_squash U_zero post) goal.goal_ty)
      then fail3 "Cannot instantiate lemma %s (with postcondition: %s) to match goal (%s)"
                              (tts goal.context tm)
                              (tts goal.context (U.mk_squash U_zero post))
  
negative.code: 
  let unify (t1 : term) (t2 : term) : tac<bool> =
      bind get (fun ps ->
      do_unify ps.main_context t1 t2)
  
  let launch_process (prog : string) (args : string) (input : string) : tac<string> =
      // The `bind idtac` thunks the tactic
  