From 75381f7356133f68637fc9bbc0a213dcfa6e2c71 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Jun 2015 15:24:49 +0200
Subject: When assuming an inductive type positive, then it is declared
 "unsafe" to the interfaces.

---
 toplevel/command.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ca925d4904..6beaf54c53 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -645,7 +645,10 @@ let do_mutual_inductive chk indl poly prv finite =
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
+  (* If [chk] is [false] (i.e. positivity is assumed) declares itself
+     as unsafe. *)
+  if not chk then Pp.feedback Feedback.AddedAxiom else ()
 
 (* 3c| Fixpoints and co-fixpoints *)
 
-- 
cgit v1.2.3