Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index e370d37fc4..23f8fbe888 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 ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ~ontop 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
@@ -13,13 +13,13 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
+  DeclareDef.declare_definition ~ontop 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
-  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
+  ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)