aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqdoc/binder.tex.out
AgeCommit message (Collapse)Author
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
This does not affect the rendering but gives better structured html/tex files.
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.