From 58b9174b229863c694ad65984b86b112c689ae10 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 31 Oct 2018 08:16:30 +0100
Subject: Revert "Merge pull request #13 from
 herbelin/master+adapt-coq8718-declaration-hooks"

This reverts commit 9e8d0b077d8021e468ec0bc117438695c0b243bf, reversing
changes made to 56c3ae6296994cc288d4931110118617bb5bb978.
---
 tuto1/src/simple_declare.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 4130bab2f4..2737793d69 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -9,9 +9,9 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
      (Option.List.cons tyopt [body]) in
   let sigma = Evd.restrict_universe_context sigma uvars in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let ucontext = Evd.evar_universe_context sigma in
+  let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
-  DeclareDef.declare_definition ident k ce ucontext imps hook
+  DeclareDef.declare_definition ident k ce ubinders imps hook
 
 let packed_declare_definition ident value_with_constraints =
   let body, ctx = value_with_constraints in
@@ -19,6 +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
-  ignore (edeclare ident k ~opaque:false sigma udecl body None [] Lemmas.no_hook)
+  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