anchor.diff:  (** 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 should_defer_flex_to_user_tac env (wl:worklist) (f:flex_t) =
     let (Flex (_, u, _)) = f in
  -  DeferredImplicits.should_defer_uvar_to_user_tac wl.tcenv u
  -
  +  let b = DeferredImplicits.should_defer_uvar_to_user_tac wl.tcenv u in
  +
  +  if Env.debug env <| Options.Other "ResolveImplicitsHook"
  +  then BU.print2 "Rel.should_defer_flex_to_user_tac for %s returning %s\n"
  +         (Print.ctx_uvar_to_string_no_reason u) (string_of_bool b);
  +
  +  b
   
   (* <quasi_pattern>:
           Given a term (?u_(bs;t) e1..en)
  
positive.code:       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
        then defer_to_user_tac env orig (flex_reason lhs ^", "^flex_reason rhs)wl
        else
  
  
negative.code:  *   for inductives, this may later include implicits for pattern variables
   *)
   
  let try_solve_single_valued_implicits env is_tac (imps:Env.implicits) : Env.implicits * bool =
    (*
     * Get the value of the implicit imp
     * Going forward, it can also return new implicits for the pattern variables
     *   (cf. the comment above about extending it to inductives)
     *)
    if is_tac then imps, false
    else
      let imp_value imp : option<term> =
        let ctx_u, r = imp.imp_uvar, imp.imp_range in
    
       let t_norm = N.normalize N.whnf_steps env ctx_u.ctx_uvar_typ in
      
        match (SS.compress t_norm).n with
        | Tm_fvar fv when S.fv_eq_lid fv Const.unit_lid ->
          r |> S.unit_const_with_range |> Some
       | Tm_refine (b, _) when U.is_unit b.sort ->
          r |> S.unit_const_with_range |> Some
       | _ -> None in
  
      let b = List.fold_left (fun b imp ->  //check that the imp is still unsolved
        if UF.find imp.imp_uvar.ctx_uvar_head |> is_none
        then match imp_value imp with
             | Some tm -> commit ([TERM (imp.imp_uvar, tm)]); true
             | None -> b
        else b) false imps in
  
      imps, b
    
  let resolve_implicits' env is_tac g =
    let must_total, forcelax =
      if is_tac then false, true
      else (not env.phase1 && not env.lax), false in
  
    let rec unresolved ctx_u =
      match (Unionfind.find ctx_u.ctx_uvar_head) with
      | Some r ->
  