anchor.diff:  
   let cases (t : term) : tac<(term * term)> =
       bind cur_goal (fun g ->
  -    let t, typ, guard = g.context.type_of g.context t in
  +    bind (__tc g.context t) (fun (t, typ, guard) ->
       let hd, args = U.head_and_args typ in
       match (U.un_uinst hd).n, args with
       | Tm_fvar fv, [(p, _); (q, _)] when S.fv_eq_lid fv PC.or_lid ->
  
positive.code: let unquote (ty : term) (tm : term) : tac<term> =
      bind cur_goal (fun goal ->
      let env = Env.set_expected_typ goal.context ty in
      let tm, typ, guard = goal.context.type_of env tm in
      Rel.force_trivial_guard env guard;
      ret tm)
  
  let uvar_env (env : env) (ty : option<typ>) : tac<term> =
      // If no type was given, add an uvar for it too!
  
negative.code: 
  let unshelve (t : term) : tac<unit> =
      bind cur_goal (fun goal ->
      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;
  