anchor.diff:  let unshelve (t : term) : tac<unit> = wrap_err "unshelve" <|
       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 "got non-trivial guard"
  -    else add_goals [{ goal with witness  = bnorm goal.context t;
  -                                goal_ty  = bnorm goal.context typ;
  -                                is_guard = false; }]))
  +    bind (must_trivial goal.context guard) (fun _ ->
  +    add_goals [{ goal with witness  = bnorm goal.context t;
  +                           goal_ty  = bnorm goal.context typ;
  +                           is_guard = false; }])))
   
   let unify (t1 : term) (t2 : term) : tac<bool> =
       bind get (fun ps ->
  
positive.code:     bind get (fun ps ->
      try ret (ps.main_context.type_of e t) with e -> fail "not typeable")
  
  let tc (t : term) : tac<typ> = wrap_err "tc" <|
      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 "got non-trivial guard"
      else ret typ
      ))
  
  let add_irrelevant_goal reason env phi opts : tac<unit> =
      bind (mk_irrelevant_goal reason env phi opts) (fun goal ->
  
negative.code:     bind cur_goal (fun goal ->
      bind (__tc goal.context t) (fun (t, typ, guard) ->
      bind (if force_guard
            then must_trivial goal.context guard
            else add_goal_from_guard "__exact typing" goal.context guard goal.opts
            ) (fun _ ->
      if do_unify goal.context typ goal.goal_ty
  