From b7e4a0dd032889422a0057162c66e39f2d0187a5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 13 May 2019 20:06:06 +0200
Subject: Remove definition-not-visible warning

This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/plugin_tutorial/tuto1')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 3c0355c92d..e9b91d5a7e 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,16 +1,16 @@
-let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
       ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data
+  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
-  ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None [])
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
-- 
cgit v1.2.3