anchor.diff:      : tac<'a>
       = kernel_tac "or_else" (fun p ->
   //        let tx = Unionfind.new_transaction () in
  -        debug p (BU.format1 "or_else: trying %s" t1.tac_name);
           match t1.tac_f p with
           | Failed _ ->
   //          Unionfind.rollback tx;
  -          debug p (BU.format2 "or_else: %s failed; trying %s" t1.tac_name t2.tac_name);
             t2.tac_f p
           | q -> q)
   
  
positive.code:                  {goal with witness=None;
                              goal_ty=a}) in
            bind dismiss (fun _ ->
            bind (add_goals new_goals) (fun _ ->
            show))
          | _ ->
            fail "Cannot split this goal; expected a conjunction")
  
  
negative.code:     = kernel_tac "bind"
          (fun p ->
  //        let tx = Unionfind.new_transaction () in //snapshot the state of the unionfind graph
              match t1.tac_f p with
              | Success (a, q) ->
                let t2 = t2 a in
                t2.tac_f q
              | Failed(msg, q) ->
      //          Unionfind.rollback tx; //and restore the snapshot in case the tactic fails
                Failed(msg, q)) //need to repack for tac<'b>
  
  