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.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/declareops.mli')

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