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/declareops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c13..870aef1d28 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -258,7 +258,9 @@ let subst_mind_body sub mib =
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
-    mind_private = mib.mind_private }
+    mind_private = mib.mind_private;
+    mind_checked_positive = mib.mind_checked_positive;
+  }
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
-- 
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/declareops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 870aef1d28..068bc498a0 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -132,7 +132,8 @@ let subst_const_body sub cb =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
-        const_inline_code = cb.const_inline_code }
+        const_inline_code = cb.const_inline_code;
+        const_checked_guarded = cb.const_checked_guarded }
 
 (** {7 Hash-consing of constants } *)
 
-- 
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/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 068bc498a0..98d2877373 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -133,7 +133,7 @@ let subst_const_body sub cb =
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code;
-        const_checked_guarded = cb.const_checked_guarded }
+        const_typing_flags = cb.const_typing_flags }
 
 (** {7 Hash-consing of constants } *)
 
-- 
cgit v1.2.3