anchor.diff:  (* ------------------------------------------------ *)
   (* <variable ops> common ops on variables           *)
   (* ------------------------------------------------ *)
  -let occurs_check (uk:ctx_uvar) t =
  +let occurs (uk:ctx_uvar) t =
       let uvars =
           Free.uvars t
           |> BU.set_elements
       in
  -    let occurs_ok =
  -        not (uvars
  -             |> BU.for_some (fun uv ->
  -                UF.equiv uv.ctx_uvar_head uk.ctx_uvar_head))
  +    let occurs =
  +        (uvars
  +        |> BU.for_some (fun uv ->
  +           UF.equiv uv.ctx_uvar_head uk.ctx_uvar_head))
       in
  +    uvars, occurs
  +let occurs_check (uk:ctx_uvar) t =
  +    let uvars, occurs = occurs uk t in
       let msg =
  -        if occurs_ok then None
  +        if not occurs then None
           else Some (BU.format2 "occurs-check failed (%s occurs in %s)"
                           (Print.uvar_to_string uk.ctx_uvar_head)
                           (Print.term_to_string t)) in
  -    uvars, occurs_ok, msg
  +    uvars, not occurs, msg
   
   let rec maximal_prefix (bs:binders) (bs':binders) : binders * (binders * binders) =
     match bs, bs' with
  
positive.code:           meet_or_join (if flip then U.mk_conj else U.mk_disj) bounds_typs env wl
        in
        let eq_prob, wl =
              new_problem wl env bound EQ this_flex None tp.loc
                  (if flip then "joining refinements" else "meeting refinements")
        in
        let _ = if Env.debug env <| Options.Other "RelCheck"
  
negative.code:   let this_flex, this_rigid = if flip then tp.lhs, tp.rhs else tp.rhs, tp.lhs in
    begin
    match (SS.compress this_rigid).n with
    | Tm_arrow (_bs, comp) ->
      //BEWARE: special treatment of Tot and GTot here
      if U.is_tot_or_gtot_comp comp
      then let flex = destruct_flex_t this_flex in
           begin
           match quasi_pattern env flex with
           | None -> giveup env "flex-arrow subtyping, not a quasi pattern" (TProb tp)
           | Some (flex_bs, flex_t) ->
             if Env.debug env <| Options.Other "RelCheck"
             then BU.print1 "Trying to solve by imitating arrow:%s\n" (string_of_int tp.pid);
             imitate_arrow (TProb tp) env wl flex flex_bs flex_t tp.relation this_rigid
           end
      else //imitating subtyping with WPs is hopeless
           solve env (attempt [TProb ({tp with relation=EQ})] wl)
    | _ ->
      if Env.debug env <| Options.Other "RelCheck"
      then BU.print1 "Trying to solve by meeting refinements:%s\n" (string_of_int tp.pid);
  