aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorPierre Letouzey2014-12-05 16:29:39 +0100
committerPierre Letouzey2014-12-09 12:14:39 +0100
commit5d2b096f29adf3d139c4de46321e26790e9b4211 (patch)
tree4f3db111c2b4821d2f8908c79cc404ede0115095 /kernel/nativecode.ml
parent484a0c35662d3bb78aa1f2cd83ffcc1b1f761968 (diff)
coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 from v8.4)
- For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before />
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions