diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-25 09:52:45 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-25 10:29:08 +0200 |
| commit | 28855216037570aeabc544ab232bb896d7a7327f (patch) | |
| tree | 0d8d5337c136675581364c86756b7775d56d0061 /checker/cic.mli | |
| parent | 476189527703aaf9caf5612e8395ce3b8ddb088f (diff) | |
Adjust checker after `Assume [Positive]`.
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index e875e40f0..82eb35bcb 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -312,6 +312,8 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) + (** {8 Data for native compilation } *) mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) |