anchor.diff:  
     | _ -> []
   
  -let mk_typ_abbrev lid uvs typars kopt t lids quals rng =
  +let mk_typ_abbrev env d lid uvs typars kopt t lids quals rng =
  +    (* fetch attributes here to support `deprecated`, just as for
  +     * TopLevelLet (see comment there) *)
  +    let attrs = List.map (desugar_term env) d.attrs in
  +    let val_attrs = Env.lookup_letbinding_quals_and_attrs env lid |> snd in
       let dd = if quals |> List.contains S.Abstract
                then Delta_abstract (incr_delta_qualifier t)
                else incr_delta_qualifier t in
  
positive.code:                    sigattrs = [];
                     sigopts = None; }
              else let t = desugar_typ env' t in
                   mk_typ_abbrev qlid [] typars kopt t [qlid] quals rng in
  
          let env = push_sigelt env se in
          let env = push_doc env qlid d.doc in
  
negative.code:                   let tpars = Subst.close_binders tpars in
                    Subst.close tpars t
            in
            [((id, d.doc), [], mk_typ_abbrev env d id uvs tpars (Some k) t [id] quals rng)]
  
          | Inl ({ sigel = Sig_inductive_typ(tname, univs, tpars, k, mutuals, _); sigquals = tname_quals }, constrs, tconstr, quals) ->
            let mk_tot t =
  