Commit ba2d414a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'fix-local-inductive' into 'master'

Remove `Local` attribute for `Inductive`

See merge request iris/iris!212
parents de7eab03 b81d90d8
Pipeline #14361 passed with stage
in 19 minutes and 49 seconds
......@@ -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