From ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 15:05:36 +0200 Subject: 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" --- kernel/term_typing.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'kernel/term_typing.mli') 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 -- cgit v1.2.3