Duplicate the type of constant entries in Proof_global.

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

7 files changed, 14 insertions, 16 deletions

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