From df40307f70d7a03b03af7ae4360a15349abc1bd0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 02:47:20 +0100
Subject: [coq overlay] Adapt to coq/coq#8705

Please apply when indicated.
---
 tuto1/src/simple_declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tuto1/src')

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 50fd170663..9d10a8ba72 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -11,7 +11,7 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ident k ce ubinders imps hook
+  DeclareDef.declare_definition ident k ce ubinders imps ~hook
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
-- 
cgit v1.2.3