From c951e2ed88437c613bd4355b32547f9c39269eed Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 20 Aug 2019 00:02:28 +0200
Subject: [declare] Move proof_entry type to declare, put interactive proof
 data on top of declare.

This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.

This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.

This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.

A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.

Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
---
 plugins/funind/gen_principle.ml  | 18 +++++++++---------
 plugins/funind/indfun_common.ml  |  2 +-
 plugins/funind/indfun_common.mli |  2 +-
 3 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 60717c6eec..352b21a15a 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1170,7 +1170,7 @@ let get_funs_constant mp =
     in
     l_const
 
-let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
+let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list =
   let exception Found_type of int in
   let env = Global.env () in
   let funs = List.map fst fas in
@@ -1244,7 +1244,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
     | Some equation ->
       Declareops.is_opaque (Global.lookup_constant equation)
   in
-  let const = {const with Proof_global.proof_entry_opaque = opacity } in
+  let const = {const with Declare.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
   if List.is_empty other_princ_types
   then
@@ -1255,8 +1255,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
       let sorts = Array.of_list sorts in
       List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let open Proof_global in
-    let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
+    let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in
     let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
     let other_result =
@@ -1299,10 +1298,10 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
            let princ_body =
              Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
            in
-           {const with
-              proof_entry_body =
-                (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
-              proof_entry_type = Some scheme_type
+           { const with
+             Declare.proof_entry_body =
+               (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
+             proof_entry_type = Some scheme_type
            }
       )
       other_fun_princ_types
@@ -1358,7 +1357,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
              Array.of_list
                (List.map
                   (fun entry ->
-                     (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
+                     (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))),
+                      EConstr.of_constr (Option.get entry.Declare.proof_entry_type ))
                   )
                   (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
                )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7719705138..ba37b9b461 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -115,7 +115,7 @@ open DeclareDef
 let definition_message = Declare.definition_message
 
 let save name const ?hook uctx scope kind =
-  let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
+  let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 16beaaa3c7..34fb10bb67 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -44,7 +44,7 @@ val make_eq : unit -> EConstr.constr
 
 val save
   :  Id.t
-  -> Evd.side_effects Proof_global.proof_entry
+  -> Evd.side_effects Declare.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> DeclareDef.locality
-- 
cgit v1.2.3