diff options
Diffstat (limited to 'proofs/proof_using.mli')
| -rw-r--r-- | proofs/proof_using.mli | 4 |
1 files changed, 4 insertions, 0 deletions
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 |