Skip to content

A Coq bug printing spurious parentheses has been fixed.

Hugo Herbelin requested to merge herbelin/iris-coq:master+consequence-coq-pr9214-printing-bug-fixed into master

We adapt iris printing tests to take into account this "improvement". See Coq PR#9214.

Note: this needs to be done synchronously with the merge of Coq #9214 since Iris is part of Coq Continuous Integration.

Merge request reports