ProofGeneral
PG sends wrong command to coqtop when printing module members.
This is maybe a bit of a silly edge case, but...
Print Nat.
works, but then when you type...
Print Nat.zero.
After running Print Nat, then if you try to execute this command it will say:
Error: Syntax error: illegal begin of vernac.
Presumably because it's trying to send zero. to coqtop, instead of the full Print Nat.zero. If you back up and run the full command again it works as expected. PG just seems to be unaware that the . after Nat changes meaning.
I think this is a known issue, and I don't have a good story to fix it. I discussed it briefly at https://github.com/FStarLang/fstar-mode.el/issues/61#issuecomment-308785004 a while back.
Would you expect that when you type something just after the locked region (with no separating space) it would behave as if the last dot of the region was edited? It makes sense but I wonder if people will find this more annoying than useful. It would certainly make pg more robust. Currently pg behaves incorrectly in this case anyway (accepting the command whereas it is sticked to the previous one.
It seems possible. Actually it may just be a matter of making the locked region overlay "opened on the right".
