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.
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6494e90a03..ce7d149ae1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -414,7 +414,7 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V
   match fixpoint_exprl with
     | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
-      ComDefinition.do_definition ~ontop:pstate
+      ComDefinition.do_definition
         ~program_mode:false
 	fname
         (Decl_kinds.Global,false,Decl_kinds.Definition) pl
-- 
cgit v1.2.3