From 7efaf86882488034e6545505e1eda7d6e1a6ce14 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 8 Apr 2018 09:35:26 +0200
Subject: [vernac] Adapt to removal of imperative proof state.

---
 vernac/declareDef.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7dcd098183..052832244b 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,12 +33,12 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
       let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-      let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in
+      let () = if Option.has_some ontop then warn_definition_not_visible ident in
       VarRef ident
   | Discharge | Local | Global ->
       let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +57,9 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   end;
   gr
 
-let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ?hook_data ce pl imps
+  declare_definition ~ontop f kind ?hook_data ce pl imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
-- 
cgit v1.2.3