From 77fc6ad50fb2bd95d19ecaee36fa34c7931a2bc1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Apr 2020 23:07:36 -0400
Subject: [declare] Remove `declare_private_constant` from the public API.

This is an internal function for scheme declaration handled properly
now, we can also remove `pure_definition_entry` which is IMO good too.
---
 vernac/declare.mli | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/vernac/declare.mli b/vernac/declare.mli
index 73e0d7cd04..a551c621c4 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -160,16 +160,6 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
-(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
-val pure_definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
-  -> ?inline:bool
-  -> ?types:types
-  -> ?univs:Entries.universes_entry
-  -> constr
-  -> unit proof_entry
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** [declare_constant id cd] declares a global declaration
@@ -187,14 +177,6 @@ val declare_constant
   -> Evd.side_effects constant_entry
   -> Constant.t
 
-val declare_private_constant
-  :  ?role:Evd.side_effect_role
-  -> ?local:import_status
-  -> name:Id.t
-  -> kind:Decls.logical_kind
-  -> unit proof_entry
-  -> Constant.t * Evd.side_effects
-
 (** [inline_private_constants ~sideff ~uctx env ce] will inline the
    constants in [ce]'s body and return the body plus the updated
    [UState.t].
-- 
cgit v1.2.3