Remove definition-not-visible warning

This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.

11 files changed, 37 insertions, 55 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 3c0355c92d..e9b91d5a7e 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,16 +1,16 @@
-let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
       ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data
+  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None [])
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6494e90a03..ce7d149ae1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -414,7 +414,7 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V
   match fixpoint_exprl with
     | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
-      ComDefinition.do_definition ~ontop:pstate
+      ComDefinition.do_definition
         ~program_mode:false
 	fname
         (Decl_kinds.Global,false,Decl_kinds.Definition) pl
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 27e31f486d..635751bb24 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,7 +43,7 @@ let should_axiom_into_instance = function
     true
   | Global | Local -> !axiom_into_instance
 
-let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
 match local with
 | Discharge when Lib.sections_are_opened () ->
   let ctx = match ctx with
@@ -53,11 +53,6 @@ match local with
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
-  let () =
-    if not !Flags.quiet && Option.has_some pstate then
-    Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
-    strbrk " is not visible from current goals")
-  in
   let r = VarRef ident in
   let () = maybe_declare_manual_implicits true r imps in
   let env = Global.env () in
@@ -101,11 +96,11 @@ let next_uctx =
   | Polymorphic_entry _ as uctx -> uctx
   | Monomorphic_entry _ -> empty_uctx
 
-let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
   let refs, status, _ =
     List.fold_left (fun (refs,status,uctx) id ->
       let ref',u',status' =
-        declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in
+        declare_assumption is_coe k (c,uctx) pl imps false nl id in
       (ref',u')::refs, status' && status, next_uctx uctx)
       ([],true,uctx) idl
   in
@@ -137,7 +132,7 @@ let process_assumptions_udecls kind l =
   in
   udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
 
-let do_assumptions ~pstate ~program_mode kind nl l =
+let do_assumptions ~program_mode kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let udecl, l = process_assumptions_udecls kind l in
@@ -183,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l =
   let ubinders = Evd.universe_binders sigma in
   pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
       let t = replace_vars subst t in
-      let refs, status' = declare_assumptions ~pstate  idl is_coe kind (t,uctx) ubinders imps nl in
+      let refs, status' = declare_assumptions  idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
@@ -231,7 +226,7 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context ~pstate poly l =
+let context poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -296,12 +291,12 @@ let context ~pstate poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus = match b with
       | None ->
-        pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
+        pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
+        let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 7c64317b70..8f37bc0ba4 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -16,8 +16,7 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions
-  :  pstate:Proof_global.t option
-  -> program_mode:bool
+  : program_mode:bool
   -> locality * polymorphic * assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
@@ -26,8 +25,7 @@ val do_assumptions
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
-  :  pstate:Proof_global.t option
-  -> coercion_flag
+  : coercion_flag
   -> assumption_kind
   -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
@@ -42,8 +40,7 @@ val declare_assumption
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
 val context
-  :  pstate:Proof_global.t option
-  -> Decl_kinds.polymorphic
+  : Decl_kinds.polymorphic
   -> local_binder_expr list
   -> bool
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d2c986fe5c..4cae4b8a74 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,7 +79,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
     interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
   in
@@ -104,4 +104,4 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-    ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps)
+    ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 12853d83e0..fa4860b079 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,8 +17,7 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  ontop:Proof_global.t option
-  -> program_mode:bool
+  : program_mode:bool
   -> ?hook:Lemmas.declaration_hook
   -> Id.t
   -> definition_kind
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1912646ffd..00f19f545c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -284,7 +284,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -319,7 +319,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
     let evd = Evd.restrict_universe_context evd vars in
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
-    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames;
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 052832244b..bdda3314ca 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,12 +14,6 @@ open Entries
 open Globnames
 open Impargs
 
-let warn_definition_not_visible =
-  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
-    Pp.(fun ident ->
-        strbrk "Section definition " ++
-        Names.Id.print ident ++ strbrk " is not visible from current goals")
-
 let warn_local_declaration =
   CWarnings.create ~name:"local-declaration" ~category:"scope"
     Pp.(fun (id,kind) ->
@@ -33,12 +27,11 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
       let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-      let () = if Option.has_some ontop then warn_definition_not_visible ident in
       VarRef ident
   | Discharge | Local | Global ->
       let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +50,9 @@ let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
   end;
   gr
 
-let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition ~ontop f kind ?hook_data ce pl imps
+  declare_definition f kind ?hook_data ce pl imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 8e4f4bf7fb..c4500d0a6b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,8 +14,7 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition
-  :  ontop:Proof_global.t option
-  -> Id.t
+  : Id.t
   -> definition_kind
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> Safe_typing.private_constants Entries.definition_entry
@@ -24,8 +23,7 @@ val declare_definition
   -> GlobRef.t
 
 val declare_fix
-  :  ontop:Proof_global.t option
-  -> ?opaque:bool
+  : ?opaque:bool
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> definition_kind
   -> UnivNames.universe_binders
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f768278dd7..46c4422d17 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -454,7 +454,7 @@ let obligation_substitution expand prg =
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
-let declare_definition ~ontop prg =
+let declare_definition prg =
   let varsubst = obligation_substitution true prg in
   let body, typ = subst_prog varsubst prg in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
@@ -473,7 +473,7 @@ let declare_definition ~ontop prg =
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
-  DeclareDef.declare_definition ~ontop prg.prg_name
+  DeclareDef.declare_definition prg.prg_name
     prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
@@ -552,7 +552,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
-  let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -759,7 +759,7 @@ let update_obls prg obls rem =
     else (
       match prg'.prg_deps with
       | [] ->
-          let kn = declare_definition ~ontop:None prg' in
+          let kn = declare_definition prg' in
 	    progmap_remove prg';
 	    Defined kn
       | l ->
@@ -1110,7 +1110,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
-    let cst = declare_definition ~ontop:None prg in
+    let cst = declare_definition prg in
       Defined cst)
   else (
     let len = Array.length obls in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1d134f3a9..918852239a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -605,7 +605,7 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
         | Some r ->
           let sigma, env = get_current_or_global_context ~pstate in
           Some (snd (Hook.get f_interp_redexp env sigma r)) in
-      ComDefinition.do_definition ~ontop:pstate ~program_mode name
+      ComDefinition.do_definition ~program_mode name
         (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
       pstate
   )
@@ -632,7 +632,7 @@ let vernac_exact_proof ~pstate c =
   if not status then Feedback.feedback Feedback.AddedAxiom;
   pstate
 
-let vernac_assumption ~atts ~pstate discharge kind l nl =
+let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
@@ -642,7 +642,7 @@ let vernac_assumption ~atts ~pstate discharge kind l nl =
       List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
-  let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in
+  let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let is_polymorphic_inductive_cumulativity =
@@ -1075,8 +1075,8 @@ let vernac_declare_instance ~atts sup inst pri =
   Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
   Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
 
-let vernac_context ~pstate ~poly l =
-  if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
+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
@@ -2300,7 +2300,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     unsupported_attributes atts;
     vernac_require_open_proof ~pstate (vernac_exact_proof c)
   | VernacAssumption ((discharge,kind),nl,l) ->
-    with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl;
+    with_def_attributes ~atts vernac_assumption discharge kind l nl;
     pstate
   | VernacInductive (cum, priv, finite, l) ->
     vernac_inductive ~atts cum priv finite l;
@@ -2383,7 +2383,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     with_def_attributes ~atts vernac_declare_instance sup inst info;
     pstate
   | VernacContext sup ->
-    let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in
+    let () = vernac_context ~poly:(only_polymorphism atts) sup in
     pstate
   | VernacExistingInstance insts ->
     with_section_locality ~atts vernac_existing_instance insts;