Fix an identifier (#1830) #15

Job	Run time
Build on macOS (Coq 8.16)	15m 18s
Sanity Checks	28s
Build on Linux (Coq latest)	7m 33s
Build SetHITs (Coq latest)	58s
Build on Linux (Coq dev)	1h 16m 22s
Build SetHITs (Coq dev)	3m 54s
Build largecatmodules (Coq latest)	1m 20s
Build largecatmodules (Coq dev)	7m 9s
Build GrpdHITs (Coq latest)	1m 54s
Build TypeTheory (Coq latest)	1m 4s
Build TypeTheory (Coq dev)	4m 33s
	2h 0m 33s

Provide feedback