diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 14:40:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 14:42:42 +0200 |
| commit | 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 (patch) | |
| tree | b75dbe069252890885fe7929aa8614e40b631359 /toplevel | |
| parent | 875f235dd0413faa34f7d46afc25d2eb90e386e5 (diff) | |
Cleanup API, making inference_hook optional
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6723a8b48..f67f6f91c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -449,7 +449,7 @@ let vernac_notation locality local = (* Gallina *) let start_proof_and_print k l hook = - let use_hook = + let inference_hook = if Flags.is_program_mode () then let hook env sigma ev = let tac = !Obligations.default_tactic in @@ -468,7 +468,7 @@ let start_proof_and_print k l hook = in Some hook else None in - start_proof_com use_hook k l hook + start_proof_com ?inference_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) |