From 28855216037570aeabc544ab232bb896d7a7327f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Thu, 25 Jun 2015 09:52:45 +0200
Subject: Adjust checker after `Assume [Positive]`.

---
 checker/cic.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'checker/cic.mli')

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) *)
-- 
cgit v1.2.3


From 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 15 Jun 2016 12:16:18 +0200
Subject: Fixing the checker.

This is a stupid fix that only allows to take into account the change in
memory layout. The check will simply fail when encountering a unguarded
inductive or (co)fixpoint.
---
 checker/cic.mli   | 13 ++++++++++++-
 checker/values.ml |  8 ++++++--
 2 files changed, 18 insertions(+), 3 deletions(-)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index 82eb35bcb..cac2384fc 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -208,6 +208,15 @@ type constant_def =
 
 type constant_universes = Univ.universe_context
 
+(** The [typing_flags] are instructions to the type-checker which
+    modify its behaviour. The typing flags used in the type-checking
+    of a constant are tracked in their {!constant_body} so that they
+    can be displayed to the user. *)
+type typing_flags = {
+  check_guarded : bool; (** If [false] then fixed points and co-fixed
+                            points are assumed to be total. *)
+}
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
@@ -216,7 +225,9 @@ type constant_body = {
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
-    const_inline_code : bool }
+    const_inline_code : bool;
+    const_typing_flags : typing_flags;
+}
 
 (** {6 Representation of mutual inductive types } *)
 
diff --git a/checker/values.ml b/checker/values.ml
index cf56bbd98..5f67b17d3 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 6f563f1f75706b28e5d3e3ef59e1681c  checker/cic.mli
+MD5 27a5893c01d6f80e7a8741ef98874e63  checker/cic.mli
 
 *)
 
@@ -208,6 +208,9 @@ let v_projbody =
   v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
 			      v_constr|]
 
+let v_typing_flags =
+  v_tuple "typing_flags" [|v_bool|]
+
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
@@ -216,7 +219,8 @@ let v_cb = v_tuple "constant_body"
     v_bool;
     v_context;
     Opt v_projbody;
-    v_bool|]
+    v_bool;
+    v_typing_flags|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
   [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|]
-- 
cgit v1.2.3