diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 16:10:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 17:55:47 +0200 |
| commit | 476189527703aaf9caf5612e8395ce3b8ddb088f (patch) | |
| tree | 3970249922178369077408ba25b7becafee36998 /checker/cic.mli | |
| 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 'checker/cic.mli')
0 files changed, 0 insertions, 0 deletions