Commit 2026-10-24 08:53 692d2753

fix: setting pp.mdata to true breaks @[pp_with_univ] (#43981) This PR fixes an issue where turning on pp.mdata causes constants tagged with @[pp_with_univ] to print as

[mdata pp.universes:true]
  [mdata pp.universes:true]
    [mdata pp.universes:true]
      [mdata pp.universes:true]
        [mdata pp.universes:true]
          [mdata pp.universes:true] [mdata pp.universes:true] [mdata pp.universes:true] [mdata pp.universes:true] ⋯

When pp.mdata is set to true, expressions with mdata are printed by first printing the mdata and the printing the bare expression underneath. This breaks @[pp_with_univ] which works by applying mdata setting pp.universes to true onto the constant name, and then redelaborating the new expression containing mdata. This causes an infinite loop the the delaborator since @[pp_with_univ] applies the mdata, and then since pp.mdata is true the mdata is removed before delaborating the constant, which then has mdata applied again, and so on. We fix the issue by instead having the implementation of @[pp_with_univ] directly set the pp.universes option, instead of delegating it to delabMData with a metadata.