anchor.diff:        else solve_t_flex_flex env (make_prob_eq orig) wl lhs rhs
   
       | EQ ->
  -      if should_defer_flex_to_user_tac wl lhs || should_defer_flex_to_user_tac wl rhs
  +      if should_defer_flex_to_user_tac env wl lhs || should_defer_flex_to_user_tac env wl rhs
         then defer_to_user_tac env orig (flex_reason lhs ^", "^flex_reason rhs)wl
         else
   
  
positive.code: (** If the head uvar of the flex term is tagged with a `Ctx_uvar_meta_attr a`
      and if a term tagged with attribute `a` is in scope,
      then this problem should be deferred to a tactic *)
  let should_defer_flex_to_user_tac (wl:worklist) (f:flex_t) =
    let (Flex (_, u, _)) = f in
    DeferredImplicits.should_defer_uvar_to_user_tac wl.tcenv u
  
  
  (* <quasi_pattern>:
          Given a term (?u_(bs;t) e1..en)
  
negative.code:     then BU.print1 "//////////////////////////ResolveImplicitsHook: resolve_implicits////////////\n\
                      guard = %s\n"
                      (guard_to_string env g);
      resolve_implicits' env false g
  
  let resolve_implicits_tac env g = resolve_implicits' env true  g
  
  let force_trivial_guard env g =
      if Env.debug env <| Options.Other "ResolveImplicitsHook"
  