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