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).

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index e093a27728..391524ebda 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -246,7 +246,7 @@ let get_roles export eff =
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
-  not (flags.check_universes && flags.check_guarded)
+  not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 let define_constant ~side_effect ~name cd =
   let open Proof_global in
-- 
cgit v1.2.3