aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqdoc/binder.v
AgeCommit message (Collapse)Author
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697.