Merge PR #10674: [declare] Move proof_entry type to declare, put interactive proof data on top of declare.

Reviewed-by: ppedrot

10 files changed, 31 insertions, 62 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 57de719cb4..9745358ba2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
   in
   if program_mode then
     let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in
+    let (c,ctx), sideff = Future.force ce.Declare.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.Proof_global.proof_entry_type with
+    let typ = match ce.Declare.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 db0c102e14..01505d0733 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -41,5 +41,5 @@ val interp_definition
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Evd.side_effects Proof_global.proof_entry *
+  -> Evd.side_effects Declare.proof_entry *
      Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 5e4f2dcd34..1926faaf0e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -44,7 +44,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
-  let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
+  let fix_exn = Future.fix_exn_of ce.proof_entry_body in
   let gr = match scope with
   | Discharge ->
       let () =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 606cfade46..54a0c9a7e8 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -45,7 +45,7 @@ val declare_definition
   -> kind:Decls.definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
-  -> Evd.side_effects Proof_global.proof_entry
+  -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
   -> GlobRef.t
 
@@ -66,7 +66,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 Proof_global.proof_entry
+  Evd.evar_map * Evd.side_effects Declare.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 c5cbb095ca..e3cffa8523 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
       if get_shrink_obligations () && not poly then shrink_body body ty
       else ([], body, ty, [||])
     in
-    let body =
-      ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
-    in
-    let ce =
-      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
+    let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant ~name:obl.obl_name
@@ -495,12 +485,11 @@ type obligation_qed_info =
   }
 
 let obligation_terminator entries uctx { name; num; auto } =
-  let open Proof_global in
   match entries with
   | [entry] ->
     let env = Global.env () in
-    let ty = entry.proof_entry_type in
-    let body, eff = Future.force entry.proof_entry_body in
+    let ty = entry.Declare.proof_entry_type in
+    let body, eff = Future.force entry.Declare.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
@@ -514,7 +503,7 @@ let obligation_terminator entries uctx { name; num; auto } =
     let obls, rem = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
-      match obl.obl_status, entry.proof_entry_opaque with
+      match obl.obl_status, entry.Declare.proof_entry_opaque with
       | (_, Evar_kinds.Expand), true -> err_not_transp ()
       | (true, _), true -> err_not_transp ()
       | (false, _), true -> Evar_kinds.Define true
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 2a8fa734b3..7d8a112cc6 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -76,7 +76,7 @@ type obligation_qed_info =
   }
 
 val obligation_terminator
-  : Evd.side_effects Proof_global.proof_entry list
+  : Evd.side_effects Declare.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 cf87646905..a6c577a878 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -98,20 +98,11 @@ let () =
 
 (* Util *)
 
-let define ~poly name sigma c t =
+let define ~poly name sigma c types =
   let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
   let univs = Evd.univ_entry ~poly sigma in
-  let open Proof_global in
-  let kn = f ~name
-    (DefinitionEntry
-      { 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;
-      }) in
+  let entry = Declare.definition_entry ~univs ?types c in
+  let kn = f ~name (DefinitionEntry entry) in
   definition_message name;
   kn
 
@@ -412,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
-    let cst = define ~poly fi sigma proof_output (Some decltype) in
+    let cst = define ~poly fi sigma decl (Some decltype) in
     GlobRef.ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -534,7 +524,6 @@ let do_combined_scheme name schemes =
       schemes
   in
   let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
   (* It is possible for the constants to have different universe
      polymorphism from each other, however that is only when the user
      manually defined at least one of them (as Scheme would pick the
@@ -542,7 +531,7 @@ let do_combined_scheme name schemes =
      some other polymorphism they can also manually define the
      combined scheme. *)
   let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
-  ignore (define ~poly name.v sigma proof_output (Some typ));
+  ignore (define ~poly name.v sigma body (Some typ));
   fixpoint_message None [name.v]
 
 (**********************************************************************)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7809425a10..42d1a1f3fc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function
   | possible_indexes ->
     (* Try all combinations... not optimal *)
     let env = Global.env() in
-    let open Proof_global in
     { const with
-      proof_entry_body =
-        Future.chain const.proof_entry_body
+      Declare.proof_entry_body =
+        Future.chain const.Declare.proof_entry_body
           (fun ((body, ctx), eff) ->
              match Constr.kind body with
              | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info =
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
-    let fix_exn = Future.fix_exn_of const.proof_entry_body in
+    let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
-      let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
+      let should_suggest = const.Declare.proof_entry_opaque &&
+                           Option.is_empty const.Declare.proof_entry_secctx in
       let open DeclareDef in
       let r = match scope with
         | Discharge ->
@@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~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 Proof_global.proof_entry_opaque = false } in
+  let f_def = { f_def with Declare.proof_entry_opaque = false } in
   let f_kind = Decls.(IsDefinition Definition) in
   let f_def = Declare.DefinitionEntry f_def in
   let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
@@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~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 Proof_global.(lemma_def.proof_entry_type) with
+    match lemma_def.Declare.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 Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
-  let lemma_def = let open Proof_global in
+  let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+  let lemma_def =
     { lemma_def with
-      proof_entry_body = lemma_body;
+      Declare.proof_entry_body = lemma_body;
       proof_entry_type = Some lemma_type }
   in
   let lemma_def = Declare.DefinitionEntry lemma_def in
@@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info =
   let { Info.hook; scope; impargs; other_thms } = info in
   if List.length entries <> 1 then
     user_err Pp.(str "Admitted does not support multiple statements");
-  let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+  let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
   let poly = match proof_entry_universes with
     | Entries.Monomorphic_entry _ -> false
     | Entries.Polymorphic_entry (_, _) -> true in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 37fe0df0ee..5d153fa8be 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         ~name ~poly ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
+    let (body, eff) = Future.force entry.Declare.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.Proof_global.proof_entry_type, Evd.evar_universe_context ctx')
+    Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx')
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = CErrors.push exn in
diff --git a/vernac/record.ml b/vernac/record.ml
index 86745212e7..11237f3873 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -340,16 +340,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-                  let open Proof_global in
-		  let entry = {
-                    proof_entry_body =
-                      Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
-                    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 entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
                   let kind = Decls.IsDefinition kind in
                   let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
 		  let constr_fip =