Duplicate the type of constant entries in Proof_global.

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

6 files changed, 75 insertions, 48 deletions

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