anchor.diff:          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))
  +        fail1 "Not a disjunction: %s" (N.term_to_string g.context typ)))
   
   let set_options (s : string) : tac<unit> =
       bind cur_goal (fun g ->
  
positive.code: 
  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) ->
      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;
  
negative.code:     let goal = { context = env; witness = u; goal_ty = typ; opts = opts; is_guard = false } in
      ret goal)
  
  let __tc (e : env) (t : term) : tac<(term * typ * guard_t)> =
      bind get (fun ps ->
      try ret (ps.main_context.type_of e t) with e -> fail "not typeable")
  
  let tc (t : term) : tac<typ> =
      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 "tc: got non-trivial guard"
      else ret typ
  