Unverified Commit b81d90d8 authored by Maxime Dénès's avatar Maxime Dénès
Browse files

Remove `Local` attribute for `Inductive`

This was a noop and will soon be an error (until `Inductive` properly
supports locality attributes). See https://github.com/coq/coq/pull/9410
parent 5221eb39
......@@ -143,7 +143,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"|].
Local Inductive esel_pat :=
Inductive esel_pat :=
| ESelPure
| ESelIdent : bool ident esel_pat.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment