Take Suggest Proof Using outside the kernel.

Also add an output test for Suggest Proof Using.

This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"

For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"

7 files changed, 98 insertions, 32 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0c0b910e1..22e109b01 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -367,7 +367,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       cook_context = None;
     }
 
-let record_aux env s_ty s_bo suggested_expr =
+let record_aux env s_ty s_bo =
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
@@ -376,10 +376,7 @@ let record_aux env s_ty s_bo suggested_expr =
           if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
-  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
-
-let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
-let set_suggest_proof_using f = suggest_proof_using := f
+  Aux_file.record_in_aux "context_used" v
 
 let build_constant_declaration kn env result =
   let open Cooking in
@@ -425,16 +422,13 @@ let build_constant_declaration kn env result =
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            let expr =
-              !suggest_proof_using (Constant.to_string kn)
-                env vars ids_typ context_ids in
-            if !Flags.record_aux_file then record_aux env ids_typ vars expr;
+            if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.record_aux_file then
-          record_aux env Id.Set.empty Id.Set.empty "";
+          record_aux env Id.Set.empty Id.Set.empty;
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
@@ -618,14 +612,10 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let context_ids = List.map NamedDecl.get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
-       let expr =
-         !suggest_proof_using (Id.to_string id)
-           env ids_def ids_typ context_ids in
-       record_aux env ids_typ ids_def expr
+       record_aux env ids_typ ids_def
   end;
   let univs = match decl.cook_universes with
   | Monomorphic_const ctx -> ctx
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 24153343e..b16f81c5a 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -77,6 +77,3 @@ val infer_declaration : trust:'a trust -> env -> constant option ->
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
-
-val set_suggest_proof_using :
-  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 1a321120c..9bfc8bada 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -105,7 +105,13 @@ let remove_ids_and_lets env s ids =
      (no_body id ||
        Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
 
-let suggest_Proof_using name env vars ids_typ context_ids =
+let record_proof_using expr =
+  Aux_file.record_in_aux "suggest_proof_using" expr
+
+(* Variables in [skip] come from after the definition, so don't count
+   for "All". Used in the variable case since the env contains the
+   variable itself. *)
+let suggest_common env ppid used ids_typ skip =
   let module S = Id.Set in
   let open Pp in
   let print x = Feedback.msg_debug x in
@@ -114,10 +120,13 @@ let suggest_Proof_using name env vars ids_typ context_ids =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
       else ppcmds in
     wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
-  let used = S.union vars ids_typ in
+
   let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
   let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
+  let all = List.fold_left (fun all d -> S.add (NamedDecl.get_id d) all)
+      S.empty (named_context env)
+  in
+  let all = S.diff all skip in
   let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
     print (str "All "        ++ pr_set false all);
@@ -133,26 +142,46 @@ let suggest_Proof_using name env vars ids_typ context_ids =
   if S.equal all all_needed then valid(str "All");
   valid (pr_set false needed);
   Feedback.msg_info (
-    str"The proof of "++ str name ++ spc() ++
+    str"The proof of "++ ppid ++ spc() ++
     str "should start with one of the following commands:"++spc()++
     v 0 (
     prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
-  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
-;;
+  if !Flags.record_aux_file
+  then
+    let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs) in
+    record_proof_using s
 
-let value = ref false
+let suggest_proof_using = ref false
 
 let _ =
   Goptions.declare_bool_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "suggest Proof using";
       Goptions.optkey   = ["Suggest";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b ->
-        value := b;
-        if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
-      ) }
+      Goptions.optread  = (fun () -> !suggest_proof_using);
+      Goptions.optwrite = ((:=) suggest_proof_using) }
+
+let suggest_constant env kn =
+  if !suggest_proof_using
+  then begin
+    let open Declarations in
+    let body = lookup_constant kn env in
+    let used = Id.Set.of_list @@ List.map NamedDecl.get_id body.const_hyps in
+    let ids_typ = global_vars_set env body.const_type in
+    suggest_common env (Constant.print kn) used ids_typ Id.Set.empty
+  end
+
+let suggest_variable env id =
+  if !suggest_proof_using
+  then begin
+    match lookup_named id env with
+    | LocalDef (_,body,typ) ->
+      let ids_typ = global_vars_set env typ in
+      let ids_body = global_vars_set env body in
+      let used = Id.Set.union ids_body ids_typ in
+      suggest_common env (Id.print id) used ids_typ (Id.Set.singleton id)
+    | LocalAssum _ -> assert false
+  end
 
 let value = ref None
 
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index c882b1827..ac2795f80 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -16,4 +16,8 @@ val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
 val to_string : Vernacexpr.section_subset_expr -> string
 
+val suggest_constant : Environ.env -> Names.Constant.t -> unit
+
+val suggest_variable : Environ.env -> Names.Id.t -> unit
+
 val get_default_proof_using : unit -> string option
diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
new file mode 100644
index 000000000..97cb0fdd8
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.out
@@ -0,0 +1,7 @@
+The proof of Top#Sec#nat should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
+The proof of foo should start with one of the following commands:
+Proof using A B. 
+Proof using All. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
new file mode 100644
index 000000000..b0b514a52
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.v
@@ -0,0 +1,31 @@
+Set Suggest Proof Using.
+
+Section Sec.
+  Variables A B : Type.
+
+  (* Some normal lemma. Sadly the internal name gets printed. *)
+  Lemma nat : Set.
+  Proof.
+    exact nat.
+  Qed.
+
+  (* Make sure All is suggested even though we add an unused variable
+  to the context. *)
+  Let foo : Type.
+  Proof.
+    exact (A -> B).
+  Qed.
+
+  (* Having a [Proof using] disables the suggestion message. *)
+  Definition bar : Type.
+  Proof using A.
+    exact A.
+  Qed.
+
+  (* Transparent definitions don't get a suggestion message. *)
+  Definition baz : Type.
+  Proof.
+    exact A.
+  Defined.
+
+End Sec.
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2c8f6ec9d..d45665dd4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -180,10 +180,14 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
   try
     let const = adjust_guardness_conditions const do_guard in
     let k = Kindops.logical_kind_of_goal_kind kind in
+    let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
     let l,r = match locality with
       | Discharge when Lib.sections_are_opened () ->
           let c = SectionLocalDef const in
           let _ = declare_variable id (Lib.cwd(), c, k) in
+          let () = if should_suggest
+            then Proof_using.suggest_variable (Global.env ()) id
+          in
           (Local, VarRef id)
       | Local | Global | Discharge ->
           let local = match locality with
@@ -192,7 +196,11 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           in
           let kn =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
-          (locality, ConstRef kn) in
+          let () = if should_suggest
+            then Proof_using.suggest_constant (Global.env ()) kn
+          in
+          (locality, ConstRef kn)
+    in
     definition_message id;
     Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r