diff options
| author | Arnaud Spiwack | 2015-06-25 09:52:45 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-06-25 10:29:08 +0200 |
| commit | 28855216037570aeabc544ab232bb896d7a7327f (patch) | |
| tree | 0d8d5337c136675581364c86756b7775d56d0061 | |
| parent | 476189527703aaf9caf5612e8395ce3b8ddb088f (diff) | |
Adjust checker after `Assume [Positive]`.
| -rw-r--r-- | checker/cic.mli | 2 | ||||
| -rw-r--r-- | checker/values.ml | 5 |
2 files changed, 5 insertions, 2 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index e875e40f0a..82eb35bcbf 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) *) diff --git a/checker/values.ml b/checker/values.ml index b2d74821d4..cf56bbd981 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli +MD5 6f563f1f75706b28e5d3e3ef59e1681c checker/cic.mli *) @@ -265,7 +265,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_bool|] let v_with = Sum ("with_declaration_body",0, |