From 8589b9b487c1e9b996975bd5dc58f548d0d9280c Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 22 Jun 2015 13:42:13 +0200
Subject: Add a field in `mutual_inductive_body` to represent mutual inductive
 whose positivity is assumed.

---
 kernel/declarations.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3f0..ef3e1bb6ae 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -184,6 +184,7 @@ 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.  *)
 }
 
 (** {6 Module declarations } *)
-- 
cgit v1.2.3


From caf8402e4af75d85223e10cba68a6a145e050dab Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 15:09:15 +0200
Subject: Add a field in `constant_body` to track constant whose
 well-foundedness is assumed.

---
 kernel/declarations.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef3e1bb6ae..591a7d404c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -74,7 +74,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_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+}
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
 
-- 
cgit v1.2.3


From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 7 Jun 2016 09:52:43 +0200
Subject: Assume totality: dedicated type rather than bool

The rational is that

1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
---
 kernel/declarations.mli | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 591a7d404c..0c085df39e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -64,6 +64,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. *)
+}
+
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
 type constant_body = {
@@ -75,7 +84,9 @@ type constant_body = {
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
-    const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+    const_typing_flags : typing_flags; (** The typing options which
+                                           were used for
+                                           type-checking. *)
 }
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-- 
cgit v1.2.3