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).
---
 tactics/declare.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 61f9c3b1c5..e093a27728 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -243,11 +243,16 @@ let get_roles export eff =
   in
   List.map map export
 
+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)
+
 let define_constant ~side_effect ~name cd =
   let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let in_section = Lib.sections_are_opened () in
-  let export, decl = match cd with
+  let export, decl, unsafe = match cd with
   | DefinitionEntry de ->
     (* We deal with side effects *)
     if not de.proof_entry_opaque then
@@ -257,19 +262,20 @@ let define_constant ~side_effect ~name cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = Entries.DefinitionEntry (cast_proof_entry de) in
-      export, ConstantEntry (PureEntry, cd)
+      export, ConstantEntry (PureEntry, cd), false
     else
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
       let de = cast_opaque_proof_entry de in
-      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
+      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false
   | ParameterEntry e ->
-    [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
+    [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict())
   | PrimitiveEntry e ->
-    [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
+    [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
   in
   let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
+  if unsafe || is_unsafe_typing_flags() then feedback_axiom();
   kn, eff, export
 
 let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
@@ -489,6 +495,7 @@ let declare_mind mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
   let (sp,kn as oname) = add_leaf id (inInductive mie) in
+  if is_unsafe_typing_flags() then feedback_axiom();
   let mind = Global.mind_of_delta_kn kn in
   let isprim = declare_projections mie.mind_entry_universes mind in
   Impargs.declare_mib_implicits mind;
-- 
cgit v1.2.3