diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 80da457670..55901bce93 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -135,6 +135,9 @@ let record_aux env s1 s2 = (keep_hyps env (Id.Set.union s1 s2))) in Aux_file.record_in_aux "context_used" v +let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) +let set_suggest_proof_using f = suggest_proof_using := f + let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in @@ -159,6 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = ignore(Future.join cst); let vars = global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in + !suggest_proof_using kn env vars ids_typ context_ids; if !Flags.compilation_mode = Flags.BuildVo then record_aux env ids_typ vars; vars diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 59706bb835..6f71ecd82f 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 |