naming conventions in SetTheory.ZFC

Stream: general

[Kevin Buzzard]

I'm still a bit hazy on the #naming conventions but one thing which has sunk in is that terms tend to start with a small letter, and types with a capital letter. So is docs#Arity.Const incorrectly capitalised? I ask because the module docstring has not been ported at all and I'm currently fixing it up.

[Floris van Doorn]

Yes, it should be Arity.const

[Kevin Buzzard]

And same question for docs#PSet.Resp.EvalAux (not a particularly well-used declaration but I'll change it anyway, I can guess the answer)