diff options
| author | Arnaud Spiwack | 2015-06-24 16:10:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-24 17:55:47 +0200 |
| commit | 476189527703aaf9caf5612e8395ce3b8ddb088f (patch) | |
| tree | 3970249922178369077408ba25b7becafee36998 /kernel | |
| parent | 75381f7356133f68637fc9bbc0a213dcfa6e2c71 (diff) | |
Make inductives that were assumed positive appear in `Print Assumptions`.
They appear as axioms of the form `Foo is positive`.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions