Skip to content
GitLab

Remove `Local` attribute for `Inductive`

Merged Maxime Dénès requested to merge maximedenes/iris-coq:fix-local-inductive into master

This was a noop and will soon be an error (until Inductive properly supports locality attributes). See https://github.com/coq/coq/pull/9410

Merge request reports