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"

1 files changed, 9 insertions, 1 deletions

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