s/|/\\coqor /g
s/Coq\(\.\|,\| \|$\)/\\Coq\1/g
s/Russell/\\\Russell/g
s/Haskell/\\\Haskell/g
s/OCaml/\\\Ocaml/g
s/ML/\\\ML/g
s/\\coqdocid{digit}/\\coqdocind{digit}/g
s/\\coqdocid{\(fingertree\|FingerTree\|node\|Node\)}/\\coqdocind{\1}/g
s/\\coqdocid{\(Empty\|Single\|Deep\)}/\\coqdocconstr{\1}/g
s/\\coqdocid{\(split\|option\|treePair\)}/\\coqdocind{\1}/g
s/\\coqdocid{\(One\|Two\|Three\|Four\|pow\\_nil\|pow\\_cons\|mkTreePair\)}/\\coqdocconstr{\1}/g
s/\\coqdocid{\(True\|False\|0\|S\|Some\|None\|mkSplit\)}/\\coqdocconstr{\1}/g
s/\\coqdocid{\(Measured\|Monoid\|Split\)}/\\coqdocind{\1}/g
s/\\coqdocid{\(monoid\|nat\|list\|vector\|pow\\_list\|JMeq\|tree\\_split\|unit\|bool\|split\|sig\|View\\_L\|View\\_R\|left\\_view\)}/\\coqdocind{\1}/g
s/\\coqdocid{\(mkMonoid\|mkTreeSplit\|mkSplit\|nil\|vnil\|vcons\|exist\|tt\|true\|false\|nil\\_left\|cons\\_left\)}/\\coqdocconstr{\1}/g
s/\\coqdocid{\(Node2\|Node3\|JMeq\\_refl\|nil\\_L\|cons\\_L\|nil\\_R\|cons\\_R\)}/\\coqdocconstr{\1}/g
s/\\coqdocid{\(struct\|wf\)}/\\coqdockw{\1}/g
s/\\{\\coqdocid{measure}/\\{\\coqdockw{measure}/g
s/'\\coqdocid{lparr'}/'\\ensuremath{\\coqdoublebar}'/g
s/'\\coqdocid{rparr'}/'\\ensuremath{\\coqdoublebar}'/g