From 14b2976cdf67db788b79d9421ce1e89bd15c7313 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Oct 2018 05:35:43 +0200
Subject: [coq] Adapt for PR #8704.

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

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 10fa640548..2737793d69 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -19,7 +19,7 @@ let packed_declare_definition ident value_with_constraints =
   let k = (Decl_kinds.Global,
            Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  let nohook = Lemmas.mk_hook (fun _ x -> x) in
+  let nohook = Lemmas.mk_hook (fun _ x -> ()) in
   ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
 
 (* But this definition cannot be undone by Reset ident *)
-- 
cgit v1.2.3