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"
---
 proofs/proof_using.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'proofs/proof_using.mli')

diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index c882b1827a..ac2795f806 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -16,4 +16,8 @@ val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
 val to_string : Vernacexpr.section_subset_expr -> string
 
+val suggest_constant : Environ.env -> Names.Constant.t -> unit
+
+val suggest_variable : Environ.env -> Names.Id.t -> unit
+
 val get_default_proof_using : unit -> string option
-- 
cgit v1.2.3