From fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 9 Feb 2021 16:44:36 -0800
Subject: Correctly sort the glossary

---
 doc/tools/coqrst/coqdomain.py | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index fa739e97bc..edb8db1e94 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1171,9 +1171,12 @@ class StdGlossaryIndex(Index):
     name, localname, shortname = "glossindex", "Glossary", "terms"
 
     def generate(self, docnames=None):
-        content = defaultdict(list)
+        def ci_sort(entry):
+            ((type, itemname), (docname, anchor)) = entry
+            return itemname.lower()
 
-        for ((type, itemname), (docname, anchor)) in self.domain.data['objects'].items():
+        content = defaultdict(list)
+        for ((type, itemname), (docname, anchor)) in sorted(self.domain.data['objects'].items(), key=ci_sort):
             if type == 'term':
                 entries = content[itemname[0].lower()]
                 entries.append([itemname, 0, docname, anchor, '', '', ''])
-- 
cgit v1.2.3