From b857552b6ffd5e72b5124aee9e35fc5c14607173 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jun 2016 17:44:18 +0200
Subject: Adding a default safe set of kernel typing flags to Declareops.

---
 kernel/declareops.ml  | 4 ++++
 kernel/declareops.mli | 5 +++++
 2 files changed, 9 insertions(+)

(limited to 'kernel')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 78e2f386e6..28f7e69cd4 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -14,6 +14,10 @@ open Context.Rel.Declaration
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+let safe_flags = {
+  check_guarded = true;
+}
+
 (** {6 Arities } *)
 
 let subst_decl_arity f g sub ar = 
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ad2b5d0a6c..6650b6b7b0 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -69,6 +69,11 @@ val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_
 val inductive_instance : mutual_inductive_body -> universe_instance
 val inductive_context : mutual_inductive_body -> universe_context
 
+(** {6 Kernel flags} *)
+
+(** A default, safe set of flags for kernel type-checking *)
+val safe_flags : typing_flags
+
 (** {6 Hash-consing} *)
 
 (** Here, strictly speaking, we don't perform true hash-consing
-- 
cgit v1.2.3