option name changed from RC0
This commit is contained in:
parent
0805d9f910
commit
674d476d83
|
@ -676,7 +676,7 @@ where
|
|||
|
||||
|
||||
context
|
||||
notes [[inductive_defs =true]]
|
||||
notes [[inductive_internals =true]]
|
||||
begin
|
||||
|
||||
inductive
|
||||
|
|
Loading…
Reference in New Issue