diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6b267283a..74361eb1c 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -116,5 +116,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs + mind_entry_universes = univs; + mind_entry_check_positivity = mib.mind_checked_positive; } |