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

8 files changed, 56 insertions, 72 deletions

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;
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d59d471d5f..7d365db85c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -59,7 +59,7 @@ match scope with
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
-  (r,Univ.Instance.empty,true)
+  (r,Univ.Instance.empty)
 
 | Global local ->
   let do_instance = should_axiom_into_instance kind in
@@ -84,7 +84,7 @@ match scope with
     | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
     | Monomorphic_entry _ -> Univ.Instance.empty
   in
-    (gr,inst,Lib.is_modtype_strict ())
+  (gr,inst)
 
 let interp_assumption ~program_mode sigma env impls c =
   let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
@@ -98,14 +98,13 @@ let next_uctx =
   | Monomorphic_entry _ -> empty_uctx
 
 let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
-  let refs, status, _ =
-    List.fold_left (fun (refs,status,uctx) id ->
-      let ref',u',status' =
-        declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
-      (ref',u')::refs, status' && status, next_uctx uctx)
-      ([],true,uctx) idl
+  let refs, _ =
+    List.fold_left (fun (refs,uctx) id ->
+        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
+        ref::refs, next_uctx uctx)
+      ([],uctx) idl
   in
-  List.rev refs, status
+  List.rev refs
 
 
 let maybe_error_many_udecls = function
@@ -178,15 +177,17 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
   let sigma = Evd.restrict_universe_context sigma uvars in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
-  pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) ->
+  let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) ->
       let typ = replace_vars subst typ in
-      let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
+      let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
       in
-      subst'@subst, status' && status, next_uctx uctx)
-    ([], true, uctx) l)
+      subst'@subst, next_uctx uctx)
+      ([], uctx) l
+  in
+  ()
 
 let do_primitive id prim typopt =
   if Lib.sections_are_opened () then
@@ -270,41 +271,43 @@ let context ~poly l =
           Monomorphic_entry Univ.ContextSet.empty
         end
   in
-  let fn status (name, b, t) =
+  let fn (name, b, t) =
     let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       (* Declare the universe context once *)
       let kind = Decls.(IsAssumption Logical) in
       let decl = match b with
-      | None ->
-        Declare.ParameterEntry (None,(t,univs),None)
-      | Some b ->
-        let entry = Declare.definition_entry ~univs ~types:t b in
-        Declare.DefinitionEntry entry
+        | None ->
+          Declare.ParameterEntry (None,(t,univs),None)
+        | Some b ->
+          let entry = Declare.definition_entry ~univs ~types:t b in
+          Declare.DefinitionEntry entry
       in
       let cst = Declare.declare_constant ~name ~kind decl in
       let env = Global.env () in
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst);
-      status
+      ()
     else
       let test x = match x.CAst.v with
-      | Some (Name id',_) -> Id.equal name id'
-      | _ -> false
+        | Some (Name id',_) -> Id.equal name id'
+        | _ -> false
       in
       let impl = List.exists test impls in
       let scope =
         if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
-      let nstatus = match b with
+      match b with
       | None ->
-        pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl
-               Declaremods.NoInline (CAst.make name))
+        let _, _ =
+          declare_assumption false ~scope ~poly ~kind:Decls.Context t
+            univs UnivNames.empty_binders [] impl
+            Declaremods.NoInline (CAst.make name)
+        in
+        ()
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _gr = DeclareDef.declare_definition
             ~name ~scope:DeclareDef.Discharge
             ~kind:Decls.Definition UnivNames.empty_binders entry [] in
-        Lib.sections_are_opened () || Lib.is_modtype_strict ()
-      in
-        status && nstatus
+        ()
   in
-  List.fold_left fn true (List.rev ctx)
+  List.iter fn (List.rev ctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 028ed39656..1632c3d578 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -21,7 +21,7 @@ val do_assumptions
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
-  -> bool
+  -> unit
 
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
@@ -37,7 +37,7 @@ val declare_assumption
   -> bool (** implicit *)
   -> Declaremods.inline
   -> variable CAst.t
-  -> GlobRef.t * Univ.Instance.t * bool
+  -> GlobRef.t * Univ.Instance.t
 
 (** Context command *)
 
@@ -46,6 +46,6 @@ val declare_assumption
 val context
   :  poly:bool
   -> local_binder_expr list
-  -> bool
+  -> unit
 
 val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 74c9bc2886..b6843eab33 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -323,11 +323,6 @@ let adjust_rec_order ~structonly binders rec_order =
   in
   Option.map (extract_decreasing_argument ~structonly) rec_order
 
-let check_safe () =
-  let open Declarations in
-  let flags = Environ.typing_flags (Global.env ()) in
-  flags.check_universes && flags.check_guarded
-
 let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
   let fixl = List.map (fun fix ->
       Vernacexpr.{ fix
@@ -339,13 +334,11 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
 let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
   let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   lemma
 
 let do_fixpoint ~scope ~poly l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
 
 let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -355,10 +348,8 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
 let do_cofixpoint_interactive ~scope ~poly l =
   let cofix, ntns = do_cofixpoint_common l in
   let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   lemma
 
 let do_cofixpoint ~scope ~poly l =
   let cofix, ntns = do_cofixpoint_common l in
-  declare_fixpoint_generic ~scope ~poly cofix ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  declare_fixpoint_generic ~scope ~poly cofix ntns
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
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c6e68effd7..3497e6369f 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -292,7 +292,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
 
-let do_program_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
@@ -322,19 +322,9 @@ let do_program_fixpoint ~scope ~poly l =
       do_program_recursive ~scope ~poly fixkind l
 
     | _, _ ->
-        user_err ~hdr:"do_program_fixpoint"
+        user_err ~hdr:"do_fixpoint"
           (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let check_safe () =
-  let open Declarations in
-  let flags = Environ.typing_flags (Global.env ()) in
-  flags.check_universes && flags.check_guarded
-
-let do_fixpoint ~scope ~poly l =
-  do_program_fixpoint ~scope ~poly l;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-
 let do_cofixpoint ~scope ~poly fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 6a754a0cde..adfb058942 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -336,8 +336,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
   let () = Declare.assumption_message name in
   Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
-  process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms;
-  Feedback.feedback Feedback.AddedAxiom
+  process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms
 
 let save_lemma_admitted ~(lemma : t) : unit =
   (* Used for printing in recthms *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9af8d8b67c..bc51dd46f3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -604,8 +604,7 @@ let vernac_assumption ~atts discharge kind l nl =
           match scope with
             | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax"
             | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
-  let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in
-  if not status then Feedback.feedback Feedback.AddedAxiom
+  ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
@@ -1074,9 +1073,6 @@ let vernac_declare_instance ~atts id bl inst pri =
   let global = not (make_section_locality locality) in
   Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri
 
-let vernac_context ~poly l =
-  if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom
-
 let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
   List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
@@ -2439,7 +2435,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacDeclareInstance (id, bl, inst, info) ->
     VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info)
   | VernacContext sup ->
-    VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup)
+    VtDefault(fun () -> ComAssumption.context ~poly:(only_polymorphism atts) sup)
   | VernacExistingInstance insts ->
     VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts)
   | VernacExistingClass id ->