Duplicate the type of constant entries in Proof_global.

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

14 files changed, 62 insertions, 67 deletions

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