Adapting to Coq PR#10832: formats associated to a given interpretation not taken into account (!335) · Merge requests · Iris / Iris

Hugo Herbelin requested to merge herbelin/iris-coq:master+fix-interpretation-notation-format-pr10832 into master Nov 12, 2019

This is patch to make Iris output tests consistent with the behavior of Coq after Coq PR#10832 will be merged. Not to merge now.

PR#10832 is fixing Coq issue #6082. In the present case, the format associated to the notation ";;" in theories/heap_lang/notation.v is now taken into account.

Adapting to Coq PR#10832: formats associated to a given interpretation not taken into account

Merge request reports