Duplicate the type of constant entries in Proof_global.

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

35 files changed, 195 insertions, 152 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 6a1282203a..bd61112f08 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -452,9 +452,9 @@ let restrict ctx vars =
   let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-let demote_seff_univs entry uctx =
+let demote_seff_univs universes uctx =
   let open Entries in
-  match entry.const_entry_universes with
+  match universes with
   | Polymorphic_entry _ -> uctx
   | Monomorphic_entry (univs, _) ->
     let seff = LSet.union uctx.uctx_seff_univs univs in
diff --git a/engine/uState.mli b/engine/uState.mli
index 204e97eb15..9689f2e961 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-val demote_seff_univs : 'a Entries.definition_entry -> t -> t
+val demote_seff_univs : Entries.universes_entry -> t -> t
 
 type rigid = 
   | UnivRigid
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 48eac96ab3..d49d657d38 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -19,7 +19,6 @@ open Vars
 open Namegen
 open Names
 open Pp
-open Entries
 open Tactics
 open Context.Rel.Declaration
 open Indfun_common
@@ -371,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         ignore(
           Declare.declare_constant
             name
-            (DefinitionEntry ce,
+            (Declare.DefinitionEntry ce,
              Decl_kinds.IsDefinition (Decl_kinds.Scheme))
         );
         Declare.definition_message name;
@@ -471,7 +470,7 @@ let get_funs_constant mp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -541,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
     with Option.IsNone -> (* non recursive definition *)
       false
   in
-  let const = {const with const_entry_opaque = opacity } in
+  let const = {const with Proof_global.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
   if List.is_empty other_princ_types
   then
@@ -552,7 +551,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
+    let open Proof_global in
+    let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
     let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
@@ -596,9 +596,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
              Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
            in
            {const with
-              const_entry_body =
+              proof_entry_body =
                 (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
-              const_entry_type = Some scheme_type
+              proof_entry_type = Some scheme_type
            }
       )
       other_fun_princ_types
@@ -638,7 +638,7 @@ let build_scheme fas =
        ignore
          (Declare.declare_constant
             princ_id
-            (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+            (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 3f70e870ab..b4f6f92f9c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -34,7 +34,7 @@ val generate_functional_principle :
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list
+ (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list
 
 val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
 val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 732a0d818f..17c79e0e6c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,14 +118,13 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 (* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
-open Entries
 open Decl_kinds
 open Declare
 
 let definition_message = Declare.definition_message
 
 let save id const ?hook uctx (locality,_,kind) =
-  let fix_exn = Future.fix_exn_of const.const_entry_body in
+  let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match locality with
     | Discharge ->
         let k = Kindops.logical_kind_of_goal_kind kind in
@@ -134,7 +133,7 @@ let save id const ?hook uctx (locality,_,kind) =
         VarRef id
     | Global local ->
         let k = Kindops.logical_kind_of_goal_kind kind in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
+        let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
         ConstRef kn
   in
   DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 8dd990775b..1d096fa488 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr
 
 val save
   :  Id.t
-  -> Evd.side_effects Entries.definition_entry
+  -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> Decl_kinds.goal_kind
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e7e523bb32..2020881c7c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -786,7 +786,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
           Array.of_list
             (List.map
                (fun entry ->
-                  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
+                  (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
                )
                (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
             )
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 8394ac2823..96601785b6 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -15,5 +15,5 @@ val invfun :
 val derive_correctness :
   (Evd.evar_map ref ->
    (Constr.pconstant * Sorts.family) list ->
-   'a Entries.definition_entry list) ->
+   'a Proof_global.proof_entry list) ->
    Constr.pconstant list -> Names.inductive list -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b049e3607c..2647e7449b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Namegen
 open Environ
-open Entries
 open Pp
 open Names
 open Libnames
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4c29d73038..f977ba34d2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,7 +1902,7 @@ let declare_projection n instance_id r =
     Declare.definition_entry ~types:typ ~univs term
   in
     ignore(Declare.declare_constant n 
-	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+           (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1979,7 +1979,7 @@ let add_morphism_as_parameter atts m n : unit =
   let uctx, instance = build_morphism_signature env evd m in
   let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-      (Entries.ParameterEntry
+      (Declare.ParameterEntry
          (None,(instance,uctx),None),
        Decl_kinds.IsAssumption Decl_kinds.Logical)
   in
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;
 }
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 8f66032873..e4fa5e84b4 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -70,19 +70,19 @@ let rec shrink ctx sign c t accu =
 | _ -> assert false
 
 let shrink_entry sign const =
-  let open Entries in
-  let typ = match const.const_entry_type with
+  let open Proof_global in
+  let typ = match const.proof_entry_type with
   | None -> assert false
   | Some t -> t
   in
   (* The body has been forced by the call to [build_constant_by_tactic] *)
-  let () = assert (Future.is_over const.const_entry_body) in
-  let ((body, uctx), eff) = Future.force const.const_entry_body in
+  let () = assert (Future.is_over const.proof_entry_body) in
+  let ((body, uctx), eff) = Future.force const.proof_entry_body in
   let (body, typ, ctx) = decompose (List.length sign) body typ [] in
   let (body, typ, args) = shrink ctx sign body typ [] in
   let const = { const with
-    const_entry_body = Future.from_val ((body, uctx), eff);
-    const_entry_type = Some typ;
+    proof_entry_body = Future.from_val ((body, uctx), eff);
+    proof_entry_type = Some typ;
   } in
   (const, args)
 
@@ -152,7 +152,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+  let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
   let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -161,20 +161,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.Entries.const_entry_universes with
+  let inst = match const.Proof_global.proof_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
     (* We mimic what the kernel does, that is ensuring that no additional
        constraints appear in the body of polymorphic constants. Ideally this
        should be enforced statically. *)
-    let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
+    let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in
     let () = assert (Univ.ContextSet.is_empty body_uctx) in
     EInstance.make (Univ.UContext.instance ctx)
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let effs = Evd.concat_side_effects eff
-    Entries.(snd (Future.force const.const_entry_body)) in
+    Proof_global.(snd (Future.force const.proof_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index c474a01d1c..e278729f89 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P
    save path *)
 val shrink_entry
   :  ('a, 'b) Context.Named.Declaration.pt list
-  -> 'c Entries.definition_entry
-  -> 'c Entries.definition_entry * Constr.t list
+  -> 'c Proof_global.proof_entry
+  -> 'c Proof_global.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
index a5b3c6cb45..81663b9b99 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -42,6 +42,11 @@ type constant_obj = {
   cst_locl : import_status;
 }
 
+type 'a constant_entry =
+  | DefinitionEntry of 'a Proof_global.proof_entry
+  | ParameterEntry of parameter_entry
+  | PrimitiveEntry of primitive_entry
+
 type constant_declaration = Evd.side_effects constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
@@ -146,13 +151,26 @@ let register_side_effect (c, role) =
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
-  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
-    const_entry_secctx = None;
-    const_entry_type = types;
-    const_entry_universes = univs;
-    const_entry_opaque = opaque;
-    const_entry_feedback = None;
-    const_entry_inline_code = inline}
+  let open Proof_global in
+  { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
+    proof_entry_secctx = None;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = None;
+    proof_entry_inline_code = inline}
+
+let cast_proof_entry e =
+  let open Proof_global in
+  {
+    const_entry_body = e.proof_entry_body;
+    const_entry_secctx = e.proof_entry_secctx;
+    const_entry_feedback = e.proof_entry_feedback;
+    const_entry_type = e.proof_entry_type;
+    const_entry_universes = e.proof_entry_universes;
+    const_entry_opaque = e.proof_entry_opaque;
+    const_entry_inline_code = e.proof_entry_inline_code;
+  }
 
 let get_roles export eff =
   let map c =
@@ -162,8 +180,9 @@ let get_roles export eff =
   List.map map export
 
 let define_constant ~side_effect ?(export_seff=false) id cd =
+  let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
-  let is_poly de = match de.const_entry_universes with
+  let is_poly de = match de.proof_entry_universes with
   | Monomorphic_entry _ -> false
   | Polymorphic_entry _ -> true
   in
@@ -172,21 +191,25 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
     match cd with
     | DefinitionEntry de when
         export_seff ||
-        not de.const_entry_opaque ||
+        not de.proof_entry_opaque ||
         is_poly de ->
       (* This globally defines the side-effects in the environment. *)
-      let body, eff = Future.force de.const_entry_body in
+      let body, eff = Future.force de.proof_entry_body in
       let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
       let export = get_roles export eff in
-      let de = { de with const_entry_body = Future.from_val (body, ()) } in
-      export, ConstantEntry (PureEntry, DefinitionEntry de)
+      let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+      let de = cast_proof_entry de in
+      export, ConstantEntry (PureEntry, Entries.DefinitionEntry de)
     | DefinitionEntry de ->
       let map (body, eff) = body, eff.Evd.seff_private in
-      let body = Future.chain de.const_entry_body map in
-      let de = { de with const_entry_body = body } in
-      [], ConstantEntry (EffectEntry, DefinitionEntry de)
-    | ParameterEntry _ | PrimitiveEntry _ as cd ->
-      [], ConstantEntry (PureEntry, cd)
+      let body = Future.chain de.proof_entry_body map in
+      let de = { de with proof_entry_body = body } in
+      let de = cast_proof_entry de in
+      [], ConstantEntry (EffectEntry, Entries.DefinitionEntry de)
+    | ParameterEntry e ->
+      [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
+    | PrimitiveEntry e ->
+      [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
   in
   let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
   kn, eff, export
@@ -217,11 +240,11 @@ let declare_definition ?(internal=UserIndividualRequest)
     definition_entry ?types ~univs ~opaque body
   in
     declare_constant ~internal ~local id
-      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
+      (DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
-  | SectionLocalDef of Evd.side_effects definition_entry
+  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -242,11 +265,12 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let (body, eff) = Future.force de.const_entry_body in
+      let open Proof_global in
+      let (body, eff) = Future.force de.proof_entry_body in
       let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
       let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
-      let poly, univs = match de.const_entry_universes with
+      let poly, univs = match de.proof_entry_universes with
       | Monomorphic_entry uctx -> false, uctx
       | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
@@ -256,12 +280,12 @@ let cache_variable ((sp,_),o) =
       let () = Global.push_context_set (not poly) univs in
       let se = {
         secdef_body = body;
-        secdef_secctx = de.const_entry_secctx;
-        secdef_feedback = de.const_entry_feedback;
-        secdef_type = de.const_entry_type;
+        secdef_secctx = de.proof_entry_secctx;
+        secdef_feedback = de.proof_entry_feedback;
+        secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (id, se) in
-      Explicit, de.const_entry_opaque,
+      Explicit, de.proof_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 233f0674ec..692eca8dde 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,9 +23,14 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of Evd.side_effects definition_entry
+  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
+type 'a constant_entry =
+  | DefinitionEntry of 'a Proof_global.proof_entry
+  | ParameterEntry of parameter_entry
+  | PrimitiveEntry of primitive_entry
+
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> Libobject.object_name
@@ -44,7 +49,7 @@ type internal_flag =
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
-  ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9b8ad8191e..8526bdd373 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -23,7 +23,6 @@ open Constr
 open CErrors
 open Util
 open Declare
-open Entries
 open Decl_kinds
 open Pp
 
@@ -122,15 +121,15 @@ let define internal role id c poly univs =
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
   let entry = {
-    const_entry_body =
+    Proof_global.proof_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
                        Evd.empty_side_effects);
-    const_entry_secctx = None;
-    const_entry_type = None;
-    const_entry_universes = univs;
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
+    proof_entry_secctx = None;
+    proof_entry_type = None;
+    proof_entry_universes = univs;
+    proof_entry_opaque = false;
+    proof_entry_inline_code = false;
+    proof_entry_feedback = None;
   } in
   let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 61608c577c..d8f4b66d0e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -22,7 +22,6 @@ open Namegen
 open Evd
 open Printer
 open Reductionops
-open Entries
 open Inductiveops
 open Tacmach.New
 open Clenv
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index adabb7a0a0..8447cf10db 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -11,7 +11,7 @@ let evil t f =
   let te = Declare.definition_entry
       ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
-  let tc = Declare.declare_constant t (DefinitionEntry te, k) in
+  let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
@@ -19,4 +19,4 @@ let evil t f =
       ~types:(Term.mkArrowR tc tu)
       (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
   in
-  ignore (Declare.declare_constant f (DefinitionEntry fe, k))
+  ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k))
diff --git a/vernac/class.ml b/vernac/class.ml
index 420baf7966..d5c75ed809 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -17,7 +17,6 @@ open Constr
 open Context
 open Vars
 open Termops
-open Entries
 open Environ
 open Classops
 open Declare
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 442f139827..d6a2f2727a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -29,7 +29,6 @@ module NamedDecl = Context.Named.Declaration
 (*i*)
 
 open Decl_kinds
-open Entries
 
 let set_typeclass_transparency c local b = 
   Hints.add_hints ~local [typeclasses_db]
@@ -324,7 +323,7 @@ let declare_instance_constant info global imps ?hook id decl poly sigma term ter
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
   let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in
-  let cdecl = (DefinitionEntry entry, kind) in
+  let cdecl = (Declare.DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
   Declare.definition_message id;
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
@@ -339,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
   let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-      (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
+      (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global imps (ConstRef cst)
 
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 3eb5eacd46..b0297b7c51 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -68,7 +68,7 @@ match local with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
+  let decl = (Declare.ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -273,10 +273,10 @@ let context poly l =
       (* Declare the universe context once *)
       let decl = match b with
       | None ->
-        (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
+        (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical)
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
-        (DefinitionEntry entry, IsAssumption Logical)
+        (Declare.DefinitionEntry entry, IsAssumption Logical)
       in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
       let env = Global.env () in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 853f2c9aa3..b3cc0a4236 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Util
-open Entries
 open Redexpr
 open Constrintern
 open Pretyping
@@ -86,12 +85,12 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   in
   if program_mode then
     let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.const_entry_body in
+    let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in
     assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
     assert(Univ.ContextSet.is_empty ctx);
     Obligations.check_evars env evd;
     let c = EConstr.of_constr c in
-    let typ = match ce.const_entry_type with
+    let typ = match ce.Proof_global.proof_entry_type with
       | Some t -> EConstr.of_constr t
       | None -> Retyping.get_type_of env evd c
     in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index af09a83f02..256abed6a1 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Entries
 open Decl_kinds
 open Redexpr
 open Constrexpr
@@ -41,5 +40,5 @@ val interp_definition
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Evd.side_effects definition_entry *
+  -> Evd.side_effects Proof_global.proof_entry *
      Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 23c98c97f9..6c1c23eacb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Constr
 open Context
-open Entries
 open Vars
 open Declare
 open Names
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 42327d6bdd..a467c22ede 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -10,7 +10,6 @@
 
 open Decl_kinds
 open Declare
-open Entries
 open Globnames
 open Impargs
 
@@ -38,7 +37,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ident (local, p, k) ?hook_data ce pl imps =
-  let fix_exn = Future.fix_exn_of ce.const_entry_body in
+  let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match local with
   | Discharge ->
       let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 6f9608f04a..ac4f44608b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -43,7 +43,7 @@ val declare_definition
   : Id.t
   -> definition_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> Evd.side_effects Entries.definition_entry
+  -> Evd.side_effects Proof_global.proof_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> GlobRef.t
@@ -64,7 +64,7 @@ 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 Entries.definition_entry
+  Evd.evar_map * Evd.side_effects Proof_global.proof_entry
 
 val prepare_parameter : allow_evars:bool ->
   poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 30aa347692..4936c9838d 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -155,18 +155,18 @@ let declare_obligation prg obl body ty uctx =
       ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
     in
     let ce =
-      { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
-      ; const_entry_secctx = None
-      ; const_entry_type = ty
-      ; const_entry_universes = uctx
-      ; const_entry_opaque = opaque
-      ; const_entry_inline_code = false
-      ; const_entry_feedback = None }
+      Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
+      ; proof_entry_secctx = None
+      ; proof_entry_type = ty
+      ; proof_entry_universes = uctx
+      ; proof_entry_opaque = opaque
+      ; proof_entry_inline_code = false
+      ; proof_entry_feedback = None }
     in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
-        (DefinitionEntry ce, IsProof Property)
+        (Declare.DefinitionEntry ce, IsProof Property)
     in
     if not opaque then
       add_hint (Locality.make_section_locality None) prg constant;
@@ -498,8 +498,8 @@ let obligation_terminator opq entries uctx { name; num; auto } =
   match entries with
   | [entry] ->
     let env = Global.env () in
-    let ty = entry.Entries.const_entry_type in
-    let body, eff = Future.force entry.const_entry_body in
+    let ty = entry.proof_entry_type in
+    let body, eff = Future.force entry.proof_entry_body in
     let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 70a4601ac6..f4495181b3 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -78,7 +78,7 @@ type obligation_qed_info =
 
 val obligation_terminator
   :  Proof_global.opacity_flag
-  -> Evd.side_effects Entries.definition_entry list
+  -> Evd.side_effects Proof_global.proof_entry list
   -> UState.t
   -> obligation_qed_info -> unit
 (** [obligation_terminator] part 2 of saving an obligation *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 80b3df84db..b393f33d5d 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -21,7 +21,6 @@ open CErrors
 open Util
 open Names
 open Declarations
-open Entries
 open Term
 open Constr
 open Inductive
@@ -104,15 +103,16 @@ let () =
 let define ~poly id internal sigma c t =
   let f = declare_constant ~internal in
   let univs = Evd.univ_entry ~poly sigma in
+  let open Proof_global in
   let kn = f id
     (DefinitionEntry
-      { const_entry_body = c;
-        const_entry_secctx = None;
-        const_entry_type = t;
-	const_entry_universes = univs;
-        const_entry_opaque = false;
-        const_entry_inline_code = false;
-        const_entry_feedback = None;
+      { proof_entry_body = c;
+        proof_entry_secctx = None;
+        proof_entry_type = t;
+        proof_entry_universes = univs;
+        proof_entry_opaque = false;
+        proof_entry_inline_code = false;
+        proof_entry_feedback = None;
       },
       Decl_kinds.IsDefinition Scheme) in
   definition_message id;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 400e0dfa3e..73403d9417 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -107,8 +107,9 @@ let adjust_guardness_conditions const = function
   | possible_indexes ->
   (* Try all combinations... not optimal *)
      let env = Global.env() in
-     { const with const_entry_body =
-        Future.chain const.const_entry_body
+     let open Proof_global in
+     { const with proof_entry_body =
+        Future.chain const.proof_entry_body
         (fun ((body, ctx), eff) ->
           match Constr.kind body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -448,12 +449,12 @@ let save_lemma_admitted ?proof ~(lemma : t) =
     | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
-      let { const_entry_secctx; const_entry_type } = List.hd entries in
-      if const_entry_type = None then
+      let { proof_entry_secctx; proof_entry_type } = List.hd entries in
+      if proof_entry_type = None then
         user_err Pp.(str "Admitted requires an explicit statement");
-      let typ = Option.get const_entry_type in
+      let typ = Option.get proof_entry_type in
       let ctx = UState.univ_entry ~poly:(pi2 k) universes in
-      let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in
+      let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
       finish_admitted id k (sec_vars, (typ, ctx), None) universes hook
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
@@ -500,15 +501,15 @@ let finish_proved opaque idopt po hook compute_guard =
       | Transparent -> false, true
       | Opaque      -> true, false
     in
-    assert (is_opaque == const.const_entry_opaque);
+    assert (is_opaque == const.proof_entry_opaque);
     let id = match idopt with
       | None -> id
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
-    let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+    let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
       let k = Kindops.logical_kind_of_goal_kind kind in
-      let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
+      let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
       let r = match locality with
         | Discharge ->
           let c = SectionLocalDef const in
@@ -550,8 +551,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   in
   (* The opacity of [f_def] is adjusted to be [false], as it
      must. Then [f] is declared in the global environment. *)
-  let f_def = { f_def with Entries.const_entry_opaque = false } in
-  let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
+  let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
+  let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
   let f_kn = Declare.declare_constant f f_def in
   let f_kn_term = mkConst f_kn in
   (* In the type and body of the proof of [suchthat] there can be
@@ -561,22 +562,22 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   let substf c = Vars.replace_vars [f,f_kn_term] c in
   (* Extracts the type of the proof of [suchthat]. *)
   let lemma_pretype =
-    match Entries.(lemma_def.const_entry_type) with
+    match Proof_global.(lemma_def.proof_entry_type) with
     | Some t -> t
     | None -> assert false (* Proof_global always sets type here. *)
   in
   (* The references of [f] are subsituted appropriately. *)
   let lemma_type = substf lemma_pretype in
   (* The same is done in the body of the proof. *)
-  let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
-  let lemma_def = let open Entries in
+  let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+  let lemma_def = let open Proof_global in
     { lemma_def with
-      const_entry_body = lemma_body ;
-      const_entry_type = Some lemma_type ;
-      const_entry_opaque = opaque ; }
+      proof_entry_body = lemma_body ;
+      proof_entry_type = Some lemma_type ;
+      proof_entry_opaque = opaque ; }
   in
   let lemma_def =
-    Entries.DefinitionEntry lemma_def ,
+    Declare.DefinitionEntry lemma_def ,
     Decl_kinds.(IsProof Proposition)
   in
   ignore (Declare.declare_constant name lemma_def)
@@ -597,7 +598,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 =
           | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
         in
         let entry, args = Abstract.shrink_entry local_context entry in
-        let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in
+        let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in
         let sigma, app = Evarutil.new_global sigma (ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
         sigma, cst) sigma0
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index cd8d22ac9a..aa15718452 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Printf
-open Entries
 open Decl_kinds
 
 (**
@@ -418,11 +417,11 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let (body, eff) = Future.force entry.const_entry_body in
+    let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
     let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
     Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
-    Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
+    Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx')
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = CErrors.push exn in
@@ -682,7 +681,7 @@ let admit_prog prg =
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
             let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified
-              (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
+              (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
               obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index 7cc8d9e9b9..9e3353bc54 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -342,16 +342,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
+                  let open Proof_global in
 		  let entry = {
-		    const_entry_body =
+                    proof_entry_body =
                       Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
-		    const_entry_secctx = None;
-		    const_entry_type = Some projtyp;
-                    const_entry_universes = ctx;
-		    const_entry_opaque = false;
-		    const_entry_inline_code = false;
-		    const_entry_feedback = None } in
-		  let k = (DefinitionEntry entry,IsDefinition kind) in
+                    proof_entry_secctx = None;
+                    proof_entry_type = Some projtyp;
+                    proof_entry_universes = ctx;
+                    proof_entry_opaque = false;
+                    proof_entry_inline_code = false;
+                    proof_entry_feedback = None } in
+                  let k = (Declare.DefinitionEntry entry,IsDefinition kind) in
 		  let kn = declare_constant ~internal:InternalTacticRequest fid k in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in