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.
---
 vernac/declareDef.mli | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 8e4f4bf7fb..c4500d0a6b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,8 +14,7 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition
-  :  ontop:Proof_global.t option
-  -> Id.t
+  : Id.t
   -> definition_kind
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> Safe_typing.private_constants Entries.definition_entry
@@ -24,8 +23,7 @@ val declare_definition
   -> GlobRef.t
 
 val declare_fix
-  :  ontop:Proof_global.t option
-  -> ?opaque:bool
+  : ?opaque:bool
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> definition_kind
   -> UnivNames.universe_binders
-- 
cgit v1.2.3