Remove superfluous sort.

Removing it makes no difference to the order of glossary entries,
which is determined by the "for ... sorted" statement above.

1 files changed, 1 insertions, 2 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index edb8db1e94..1ab4fe8f81 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1180,8 +1180,7 @@ class StdGlossaryIndex(Index):
             if type == 'term':
                 entries = content[itemname[0].lower()]
                 entries.append([itemname, 0, docname, anchor, '', '', ''])
-        content = sorted(content.items())
-        return content, False
+        return content.items(), False
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
     """A grammar production not included in a ``prodn`` directive.