diff options
| author | Arnaud Spiwack | 2015-06-23 09:24:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | 9a1e80524e1650311b019fedbd7e774242d80ea4 (patch) | |
| tree | aaffe224a7426e16ca33f4066d4c382e2c54fa0a /library | |
| parent | 8589b9b487c1e9b996975bd5dc58f548d0d9280c (diff) | |
Add a corresponding field in `mutual_inductive_entry` (part 1).
The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index c3181e4c75..02e6daddeb 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -366,7 +366,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; + mind_entry_check_positivity = true; }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry |