[vernac] Thread proof state to declare_assumption for warning

Not sure the warning is worth the extra parameter.

5 files changed, 37 insertions, 23 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9d9318fb77..6a67a1b5d0 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -439,7 +439,7 @@ let context ~pstate poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus = match b with
       | None ->
-        pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
+        pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 8954fde224..73e4b024ef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -76,4 +76,8 @@ val id_of_class : typeclass -> Id.t
 
 (** 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 -> local_binder_expr list -> bool
+val context
+  :  pstate:Proof_global.t option
+  -> Decl_kinds.polymorphic
+  -> local_binder_expr list
+  -> bool
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 27c5abf5ea..d7bd64067b 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = function
     true
   | Global | Local -> !axiom_into_instance
 
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption ~pstate 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
@@ -52,12 +52,11 @@ 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
-  (* XXX *)
-  (* let () =
-   *   if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
-   *   Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
-   *   strbrk " is not visible from current goals")
-   * 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 () = Typeclasses.declare_instance None true r in
@@ -97,11 +96,11 @@ let next_uctx =
   | Polymorphic_entry _ as uctx -> uctx
   | Monomorphic_entry _ -> empty_uctx
 
-let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions ~pstate 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 is_coe k (c,uctx) pl imps false nl id in
+        declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in
       (ref',u')::refs, status' && status, next_uctx uctx)
       ([],true,uctx) idl
   in
@@ -133,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 ~program_mode kind nl l =
+let do_assumptions ~pstate ~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
@@ -174,7 +173,7 @@ let do_assumptions ~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 idl is_coe kind (t,uctx) ubinders imps nl in
+      let refs, status' = declare_assumptions ~pstate 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
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2b794b001a..32914cc11b 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,8 +17,13 @@ open Decl_kinds
 
 (** {6 Parameters/Assumptions} *)
 
-val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_object_kind ->
-  Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
+val do_assumptions
+  :  pstate:Proof_global.t option
+  -> program_mode:bool
+  -> locality * polymorphic * assumption_object_kind
+  -> Declaremods.inline
+  -> (ident_decl list * constr_expr) with_coercion list
+  -> bool
 
 (************************************************************************)
 (** Internal API  *)
@@ -28,10 +33,16 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob
 
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
-val declare_assumption : coercion_flag -> assumption_kind ->
-  types in_universes_entry ->
-  UnivNames.universe_binders -> Impargs.manual_implicits ->
-  bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
-  GlobRef.t * Univ.Instance.t * bool
+val declare_assumption
+  :  pstate:Proof_global.t option
+  -> coercion_flag
+  -> assumption_kind
+  -> types in_universes_entry
+  -> UnivNames.universe_binders
+  -> Impargs.manual_implicits
+  -> bool (** implicit *)
+  -> Declaremods.inline
+  -> variable CAst.t
+  -> GlobRef.t * Univ.Instance.t * bool
 
 val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6a5f5e7b4..5d73d2e401 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -632,7 +632,7 @@ let vernac_exact_proof ~pstate c =
   if not status then Feedback.feedback Feedback.AddedAxiom;
   pstate
 
-let vernac_assumption ~atts discharge kind l nl =
+let vernac_assumption ~atts ~pstate 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 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 ~program_mode:atts.program kind nl l in
+  let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let is_polymorphic_inductive_cumulativity =
@@ -2280,7 +2280,7 @@ let interp ?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 discharge kind l nl;
+    with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl;
     pstate
   | VernacInductive (cum, priv, finite, l) ->
     vernac_inductive ~atts cum priv finite l;