anchor.diff:          bind (par_ctac c (map_ctac c) (x, xs)) (fun ((x, xs), flag) ->
           ret (x::xs, flag))
   
  -let bind_ctac
  -    (t : ctac<'a>)
  -    (f : 'a -> ctac<'b>)
  -  : ctac<'b>
  -  = fun b -> failwith ""
  +(* let bind_ctac *)
  +(*     (t : ctac<'a>) *)
  +(*     (f : 'a -> ctac<'b>) *)
  +(*   : ctac<'b> *)
  +(*   = fun b -> failwith "" *)
   
   let ctac_id (* : ctac<'a> *) =
     fun (x:'a) -> ret (x, Continue)
  
positive.code:                    (Print.term_to_string tm)
                     (Print.term_to_string ut)) (fun () ->
      ret ut)))))
  
  (* If __do_rewrite fails with "SKIP" we do nothing *)
  let do_rewrite
  
negative.code:     (tm : term)
    : tac<term>
  =
    (*
     * We skip certain terms. In particular if the term is a constant
     * which must have an argument (reify, reflect, range_of,
     * set_range_of), since typechecking will then fail, and the tactic
     * will also not be able to do anything useful. Morally, `reify` is
     * not a term, so it's fine to skip it.
     *
     * This is not perfect since if we have any other node wrapping the
     * `reify` (metadata?) this will still fail. But I don't think that
     * ever happens currently.
     *)
    let should_skip =
      match (SS.compress tm).n with
      | S.Tm_constant Const.Const_reify
      | S.Tm_constant (Const.Const_reflect _)
      | S.Tm_constant Const.Const_range_of
      | S.Tm_constant Const.Const_set_range_of ->
        true
      | _ -> false
    in
    if should_skip then ret tm else begin
  
      (* It's important to keep the original term if we want to do
       * nothing, (hence the underscore below) since after the call to
       * the typechecker, t can be elaborated and have more structure. In
  