diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-17 20:26:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
| commit | ecb032467557631ea60324c6afa55c91c133e40d (patch) | |
| tree | 831803ca1db0e73ec3cea91c52f5f2e288d12341 /toplevel/discharge.ml | |
| parent | 53ced0735f7e24735d78a02fc74588b8d9186eab (diff) | |
Reuse the typing_flags datatype for inductives.
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 74361eb1c..fcb260f51 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -117,5 +117,4 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; mind_entry_universes = univs; - mind_entry_check_positivity = mib.mind_checked_positive; } |