Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints) and [check_positive] (for (co)inductive types).

1 files changed, 1 insertions, 0 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7a553700e8..391b139496 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration
 
 let safe_flags oracle = {
   check_guarded = true;
+  check_positive = true;
   check_universes = true;
   conv_oracle = oracle;
   share_reduction = true;