From 4b81a2269919ad47c03aab5a1e578c34f3cc6ed1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Aug 2019 23:13:39 +0200
Subject: Emit Feedback.AddedAxiom in Declare instead of higher layers

This lets us remove the passing around of "status" in comassumption
and generally makes highlighting axiom adding lines in coqide more
reliable as there's no need for per-command code.

If a command adds multiple axioms it will emit AddedAxiom multiple
times, this doesn't seem to be a problem though.

We may wonder if "Fail Fail Axiom" should be highlighted as
"Axiom" (both before and after this commit it is).
---
 vernac/comInductive.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 664010c917..adbe196699 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -567,9 +567,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
-  (* If positivity is assumed declares itself as unsafe. *)
-  if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
-- 
cgit v1.2.3