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 /library | |
| parent | 53ced0735f7e24735d78a02fc74588b8d9186eab (diff) | |
Reuse the typing_flags datatype for inductives.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 4e9e68dff..f809e9742 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -354,7 +354,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; mind_entry_private = None; - mind_entry_check_positivity = true; }) +}) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry |