aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-27 15:05:36 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-10-10 23:50:22 +0200
commitffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (patch)
tree6bde0d640de16eec21b6e93b73ffac1a96e18b6c /vernac
parentb6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (diff)
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"
Diffstat (limited to 'vernac')
-rw-r--r--vernac/lemmas.ml10
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