From bc4560fa6c88aadcb2ee8312a950a7ce17fc33ee Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 5 Nov 2018 11:18:08 +0100
Subject: Split the [check_guarded] typing_flag into [check_guarded] (for
 (co)fixpoints) and [check_positive] (for (co)inductive types).

---
 kernel/declareops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declareops.ml')

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;
-- 
cgit v1.2.3