diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-27 15:05:36 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-10 23:50:22 +0200 |
| commit | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (patch) | |
| tree | 6bde0d640de16eec21b6e93b73ffac1a96e18b6c /vernac | |
| parent | b6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (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.ml | 10 |
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 |