From 1c52cde4e5f5438305e17d95435dbdcf3bf8ea00 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 14:40:00 +0200
Subject: Cleanup API, making inference_hook optional

---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6723a8b489..f67f6f91ce 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 _ _ -> ())
 
-- 
cgit v1.2.3