I wanted to upgrade Emacs (currently 26.1, from emacsformacosx.com, imported directly from High Sierra, with PG 4.5-git) on my Mac running Catalina, and discovered that Apple has made things difficult for Emacs on this version of Mac OS by introducing a "check for malicious software", which seems tricky to bypass.
I reverted to my previous Emacs version, but, since then, the .+1 notation for SSReflect nat doesn't display properly in the Coq Goals buffer of PG (my own Notations are properly managed, though). It's displayed as the standard succn constructor instead.
Does anyone have any idea what the problem might be (FWIW, I'm using the NixOS version of CoQ)?