chore: remove the coercion from String to Name#3589

Merged

kim-em merged 9 commits intoleanprover:masterfrom david-christiansen:coe-String-Name

Mar 22, 2024

+70-49

Commits on Mar 11, 2024

Commits on Mar 18, 2024

Merge remote-tracking branch 'upstream/nightly-with-mathlib' into coe-String-Name
david-christiansen
committed