anchor.diff:  let rec map (t:tac<'a>): tac<(list<'a>)> =
       mk_tac (fun ps -> run (bind (cur_goal_and_rest t (map t))
                                   (function
  -                                 | hd, None -> ret [hd]
  -                                 | hd, Some tl -> ret (hd::tl))
  +                                 | None, None -> ret []
  +                                 | Some hd, None -> ret [hd]
  +                                 | Some hd, Some tl -> ret (hd::tl))
                             ) ps)
   
   (* map_goal_term f:
  
positive.code:                       runs g on the rest of the goals
                        Collects all the remaining goals, in order sub_goals f @ sub_goals g
  *)
  let cur_goal_and_rest (f:tac<'a>) (g:tac<'b>) : tac<('a*option<'b>)>
      = bind get (fun p ->
            match p.goals with
            | [] -> fail "No more goals"
            | [_] ->
              bind f (fun a ->
              ret (a, None))
            | hd::tl ->
              bind dismiss_all (fun _ ->
              bind (add_goals [hd]) (fun _ ->
  
negative.code:             bind (add_goals tl) (fun _ ->
              bind g (fun b ->
              bind (add_goals sub_goals_f) (fun _ ->
              ret (Some a, Some b))))))))))
  
  (* or_else: try t1; if it fails, try t2 *)
  let or_else (t1:tac<'a>) (t2:tac<'a>) : tac<'a> =
  