diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 69c0aaea8..d7c96feca 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -592,7 +592,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls = impls; if_verbose msg_info (minductive_message names); if mie.mind_entry_private == None - && not (mie.mind_entry_record = Some true) then declare_default_schemes mind; mind |