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 /kernel/term_typing.mli | |
| 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 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |