Skip to content
Snippets Groups Projects
Verified Commit 570ea001 authored by Johannes Hostert's avatar Johannes Hostert
Browse files

open your eyes; your double-blindness is cured

parent 2894a20f
No related branches found
No related tags found
1 merge request!18Tree Borrows update
Pipeline #118429 passed
......@@ -4,7 +4,7 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
# Warning seems incorrect
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
theories/logic/satisfiable.v
......@@ -124,7 +124,6 @@ theories/stacked_borrows/examples/coinductive.v
## Tree Borrows
# theories/tree_borrows/helpers.v
theories/tree_borrows/locations.v
theories/tree_borrows/lang_base.v
theories/tree_borrows/notation.v
......
opam-version: "2.0"
maintainer: "Homer Simpson <homer@simpson.org>"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "Simuliris Authors"
homepage: "http://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/simuliris/issues"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment