[proof] Rework proof interface.

- deprecate the old 5-tuple accessor in favor of a view record,

- move `name` and `kind` proof data from `Proof_global` to `Proof`,
  this will prove useful in subsequent functionalizations of the
  interface, in particular this is what abstract, which lives in the
  monads, needs in order no to access global state.

- Note that `Proof.t` and `Proof_global.t` are redundant anyways.

1 files changed, 3 insertions, 3 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index e835bdcb1e..77fb49625c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1936,7 +1936,7 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
       stm_purify (fun () ->
-       let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
+       let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
        let is_ground c = Evarutil.is_ground_term sigma0 c in
        if not (
@@ -1957,7 +1957,7 @@ end = struct (* {{{ *)
         *)
         let st = Vernacstate.freeze_interp_state `No in
         ignore(stm_vernac_interp r_state_fb st ast);
-        let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
+        let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
@@ -1999,7 +1999,7 @@ end = struct (* {{{ *)
     (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
-      let goals, _, _, _, _ = Proof.proof p in
+      let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
         let f, assign =