Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layers

Reviewed-by: ppedrot

9 files changed, 62 insertions, 72 deletions

diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
new file mode 100644
index 0000000000..413805e8e9
--- /dev/null
+++ b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then
+
+    elpi_CI_REF=feedback-added-axiom
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
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 ->