aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declareops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/declareops.ml')
-rw-r--r--kernel/declareops.ml4
1 files changed, 4 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 =