Duplicate the type of constant entries in Proof_global.

This allows to desynchronize the kernel-facing API from the proof-facing one.

4 files changed, 37 insertions, 14 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e8164a14a7..cb4eabcc85 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -11,7 +11,6 @@
 open Pp
 open Util
 open Names
-open Entries
 open Environ
 open Evd
 
@@ -127,7 +126,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
     let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
-      let univs = UState.demote_seff_univs entry universes in
+      let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in
       entry, status, univs
     | _ ->
       CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
@@ -141,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
   let ce, status, univs =
     build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
-  let body, eff = Future.force ce.const_entry_body in
+  let body, eff = Future.force ce.Proof_global.proof_entry_body in
   let (cb, ctx) =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
     else body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2d3b66ff9f..d01704926a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -61,7 +61,7 @@ val use_unification_heuristics : unit -> bool
 val build_constant_by_tactic :
   Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
   EConstr.types -> unit Proofview.tactic -> 
-  Evd.side_effects Entries.definition_entry * bool *
+  Evd.side_effects Proof_global.proof_entry * bool *
     UState.t
 
 val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 0b1a7fcc03..4490fbdd64 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -24,9 +24,21 @@ module NamedDecl = Context.Named.Declaration
 
 (*** Proof Global Environment ***)
 
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 type proof_object = {
   id : Names.Id.t;
-  entries : Evd.side_effects Entries.definition_entry list;
+  entries : Evd.side_effects proof_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: UState.t;
 }
@@ -231,14 +243,14 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     let t = EConstr.Unsafe.to_constr t in
     let univstyp, body = make_body t p in
     let univs, typ = Future.force univstyp in
-    {Entries.
-      const_entry_body = body;
-      const_entry_secctx = section_vars;
-      const_entry_feedback = feedback_id;
-      const_entry_type  = Some typ;
-      const_entry_inline_code = false;
-      const_entry_opaque = opaque;
-      const_entry_universes = univs; }
+    {
+      proof_entry_body = body;
+      proof_entry_secctx = section_vars;
+      proof_entry_feedback = feedback_id;
+      proof_entry_type  = Some typ;
+      proof_entry_inline_code = false;
+      proof_entry_opaque = opaque;
+      proof_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
   { id = name; entries = entries; persistence = strength;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 15685bd9b6..4e1aa64e7b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -31,9 +31,21 @@ val compact_the_proof : t -> t
     function which takes a [proof_object] together with a [proof_end]
     (i.e. an proof ending command) and registers the appropriate
     values. *)
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 type proof_object = {
   id : Names.Id.t;
-  entries : Evd.side_effects Entries.definition_entry list;
+  entries : Evd.side_effects proof_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: UState.t;
 }