anchor.diff:  
   let unshelve (t : term) : tac<unit> =
       bind cur_goal (fun goal ->
  -    bind (try ret (goal.context.type_of goal.context t)
  -          with e -> fail "unshelve: not typeable") (fun (t, typ, guard) ->
  +    bind (__tc goal.context t) (fun (t, typ, guard) ->
       if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard)
       then fail "unshelve: got non-trivial guard"
       else add_goals [{ goal with witness  = bnorm goal.context t;
  
positive.code:         bind (if not (istrivial goal.context (U.mk_squash pre))
                then add_irrelevant_goal "apply_lemma precondition" goal.context pre goal.opts
                else ret ()) (fun _ ->
          add_goals sub_goals)))))))
  
  let destruct_eq' (typ : typ) : option<(term * term)> =
      match U.destruct_typ_as_formula typ with
  
negative.code:         bind (add_goals [g1; g2]) (fun _ ->
          ret (S.bv_to_name v_p, S.bv_to_name v_q)))
      | _ ->
          fail1 "Not a disjunction: %s" (N.term_to_string g.context typ)))
  
  let set_options (s : string) : tac<unit> =
      bind cur_goal (fun g ->
  