std_ppcmds is persistent, errors can be printed twice

The patch is very simple and naive, there is no lazy involved.
This makes a difference only for strbrk.
An extra patch may be necessary if there is a noticeable slowdown.
In any case the data type used is opaque, to ease any future optimization.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16528 85f007b7-540e-0410-9357-904b9bb8a0f7