diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 59706bb83..6f71ecd82 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -35,3 +35,6 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body + +val set_suggest_proof_using : + (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit |