From 946c6c7e58a1dfbe57445a0a1508a587193bb7c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 03:55:40 +0200
Subject: [declare] Simplify exported type of definition_entry

This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.

Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
---
 vernac/declare.ml  | 11 ++++++++---
 vernac/declare.mli |  9 +--------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index c77d4909da..7394f7f9c2 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -138,7 +138,9 @@ type 'a proof_entry = {
 
 let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
 
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+(** [univsbody] are universe-constraints attached to the body-only,
+   used in vio-delayed opaque constants and private poly universes *)
+let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
   { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
     proof_entry_secctx = section_vars;
@@ -148,6 +150,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?sect
     proof_entry_feedback = feedback_id;
     proof_entry_inline_code = inline}
 
+let definition_entry =
+  definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+
 type proof_object =
   { name : Names.Id.t
   (* [name] only used in the STM *)
@@ -241,7 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
         let utyp = UState.check_univ_decl ~poly ctx udecl in
         utyp, Univ.ContextSet.empty
     in
-    definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+    definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
   { name; entries; uctx }
@@ -998,7 +1003,7 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 647896e2f5..b380afc97d 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -144,17 +144,10 @@ val declare_variable
    for removal from the public API, use higher-level declare APIs
    instead *)
 val definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
+  :  ?opaque:bool
   -> ?inline:bool
-  -> ?feedback_id:Stateid.t
-  -> ?section_vars:Id.Set.t
   -> ?types:types
   -> ?univs:Entries.universes_entry
-  -> ?eff:Evd.side_effects
-  -> ?univsbody:Univ.ContextSet.t
-  (** Universe-constraints attached to the body-only, used in
-     vio-delayed opaque constants and private poly universes *)
   -> constr
   -> Evd.side_effects proof_entry
 
-- 
cgit v1.2.3