From f51dca0647b3213eb20a9b004372e5e6182bb29a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 3 May 2016 11:02:05 +0200
Subject: Call hooks when terminating a definition proof (bug #4663).

Also register properly the kind of definition.
---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel/vernacentries.ml')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ee11d356d..c76432ae3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -463,8 +463,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
- 	  start_proof_and_print (local,p,DefinitionBody Definition)
-	    [Some (lid,pl), (bl,t,None)] no_hook
+	  start_proof_and_print (local,p,DefinitionBody k)
+	    [Some (lid,pl), (bl,t,None)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
-- 
cgit v1.2.3