Forked from
Iris / Iris
8179 commits behind the upstream repository.
-
Maxime Dénès authored
This was a noop and will soon be an error (until `Inductive` properly supports locality attributes). See https://github.com/coq/coq/pull/9410
Maxime Dénès authoredThis was a noop and will soon be an error (until `Inductive` properly supports locality attributes). See https://github.com/coq/coq/pull/9410
