Import Coq.Strings.Ascii before using ascii notations
I don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/57743dd702b4c09b6e8d7cd171c0d7852d1da39a / https://github.com/JasonGross/iris-coq/compare/fix-for-8064
Import prim token notations before using them
This is required for compatibility with
coq/coq#8064, where prim token notations no longer
follow Require
, but instead follow Import
.
c.f. coq/coq#8064 (comment)
All changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py