From f0c393b57e89d01fd409008d3b88ea3a2ed87236 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 20 Aug 2019 20:30:32 +0200
Subject: [declare] Make `proof_entry` a private type.

Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.

This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.

So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.

To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.
---
 vernac/declareDef.mli | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index d6001f5970..1bb6620886 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -62,11 +62,16 @@ val declare_fix
   -> Impargs.manual_implicits
   -> GlobRef.t
 
-val prepare_definition : allow_evars:bool ->
-  ?opaque:bool -> ?inline:bool -> poly:bool ->
-  Evd.evar_map -> UState.universe_decl ->
-  types:EConstr.t option -> body:EConstr.t ->
-  Evd.evar_map * Evd.side_effects Declare.proof_entry
+val prepare_definition
+  :  allow_evars:bool
+  -> ?opaque:bool
+  -> ?inline:bool
+  -> poly:bool
+  -> Evd.evar_map
+  -> UState.universe_decl
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> Evd.evar_map * Evd.side_effects Declare.proof_entry
 
 val prepare_parameter : allow_evars:bool ->
   poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
-- 
cgit v1.2.3