From b857552b6ffd5e72b5124aee9e35fc5c14607173 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 78e2f386e..28f7e69cd 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 = 
-- 
cgit v1.2.3