diff --git a/_CoqProject b/_CoqProject index 3f81f7a4379372c7686ab9c83670a9ef1daaeae8..a982889c6e1eee3732cab25613e33b5ed5b9571a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -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 diff --git a/coq-simuliris.opam b/coq-simuliris.opam index 391e36d5d0be0fe42f202ba674cced8d17e06f03..198a64d6b6d336955dc94970bcdf84c8597a24dc 100644 --- a/coq-simuliris.opam +++ b/coq-simuliris.opam @@ -1,5 +1,5 @@ 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"