The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.
requested to merge herbelin/iris-coq:master+consequence-coq-pr10239-intropattern-means-simple_intropattern into master
See Coq PR#10239.
Formerly it was bound to Coq entry intropattern. This has an impact on the printing test files. Since IRIS was using explicitly simple_intropattern, I assume that this is also a fix, i.e. simple_intropattern does with Coq PR#10239 what it is expected to do. Thus, it is the printing test which should be fixed.
To be merged synchroneously with the Coq PR.