3 files changed, 13 insertions, 11 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 9d10a8ba72..e370d37fc4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
-let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let sigma = Evd.minimize_universes sigma in
   let body = EConstr.to_constr sigma body in
   let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
@@ -9,16 +9,17 @@ 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 uctx = 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 ubinders imps ~hook
+  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  let nohook = Lemmas.mk_hook (fun _ x -> ()) in
-  ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
index 9d9f894e18..663113d012 100644
--- a/doc/plugin_tutorial/tuto3/src/construction_game.ml
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -1,4 +1,5 @@
 open Pp
+open Context
 
 let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
 
@@ -32,7 +33,7 @@ let dangling_identity env evd =
   let evd, arg_type = Evarutil.new_evar env evd type_type in
 (* Notice the use of a De Bruijn index for the inner occurrence of the
   bound variable. *)
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let dangling_identity2 env evd =
@@ -40,7 +41,7 @@ let dangling_identity2 env evd =
   is meant to be a type. *)
   let evd, (arg_type, type_type) =
     Evarutil.new_type_evar env evd Evd.univ_rigid in
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
index 8f2c387d09..2d541087ce 100644
--- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -116,11 +116,11 @@ let repackage i h_hyps_id = Goal.enter begin fun gl ->
           mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
     Refine.refine ~typecheck:true begin fun evd ->
       let evd, new_goal = Evarutil.new_evar env evd
-          (mkProd (Names.Name.Anonymous,
-                     mkApp(c_H (), [| new_packed_type |]),
-                       Vars.lift 1 concl)) in
-        evd, mkApp (new_goal,
-                 [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+          (mkArrowR (mkApp(c_H (), [| new_packed_type |]))
+             (Vars.lift 1 concl))
+      in
+      evd, mkApp (new_goal,
+                  [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
       end
     end