pp.links handles unit.star badly

[eric-wieser]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

unit.star is doubly linked, which breaks formatting in doc-gen. This is a regression from #778.

Steps to Reproduce

set_option pp.links true

-- unit.starunit.star()
run_cmd tactic.pp `(()) >>= tactic.trace

Expected behavior: unit.star()

Actual behavior: unit.starunit.star()

Reproduces how often: 100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.