Update details for ForAllTy and ForAllCo in core-spec, as they
can now quantify over coercion variables.
I think the original Makefile got this right: the mng file is the one with the [[ and ]] marks, which then produces a tex file. I double-checked in the ott manual about this, and the manual (IIUC) agrees with the original usage here.
Is that the right Note?
Ok, I see. I will revert the renaming. My apologies.
Yes, it's "the last wrinkle..." in this note.