Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
!312
Avoid relying on `Export` bugs
代码
评审变更
检出分支
下载
补丁
文本差异
Maxime Dénès
requested to merge
maximedenes/iris-coq:fix-export
into
master
Sep 10, 2019
Overview
7
Commits
1
Pipelines
0
Changes
7
Expand
See
https://github.com/coq/coq/issues/10480
and
https://github.com/coq/coq/issues/10474
.
Merge request reports