From c8883873426c92778a1cac02da17e3d123beb394 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 23:35:47 +0200
Subject: [vernac] Remove unused abstraction from declaration_hook type.

"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.

We thus remove the polymorphism with the hope to be able to reify the
control later on.
---
 vernac/declareDef.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 77177dfa41..7426c128cc 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -58,9 +58,9 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k pl imps in
-  Lemmas.call_hook fix_exn hook local r
+  Lemmas.call_hook fix_exn hook local r; r
 
 let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ()))
 
-- 
cgit v1.2.3