Ah, so they were. I don't know how I overlooked that, sorry. (I guess I just missed the h at the end.)
I added the note just to make sure there is no confusion about how ungetc() works; it just rebuffers the character, so that following read or scan operations will see use it. It is not visible outside the process in any way.
In fact, you could just use getchar() or fgetc(stdin) instead of getch(), and ungetc(c, stdin) instead of ungetch(c).
You are always guaranteed to be able to push the last character you just read back into the buffer (which is what the code uses it for, only). For the code you showed, the standard functions provide the needed functionality; there is no need for the wrappers or the buffer.
(In fact, the man page says "ungetc() pushes c back to stream, cast to unsigned char, where it is available for subsequent read operations. Pushed-back characters will be returned in reverse order; only one pushback is guaranteed." It means that the char does not have to be the one you read. It also explains the odd extra input character, ((unsigned char)EOF), if you accidentally ungetc(EOF, stdin);)