diff options
| -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, |