aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/declareops.mli5
2 files changed, 9 insertions, 0 deletions
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 =
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ad2b5d0a6..6650b6b7b 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