[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.

2 files changed, 9 insertions, 9 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index b8af2bcd56..230a3207a8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.proof }) ->
-       let proof = Proof_global.proof_of_state proof in
-       let focused, r1, r2, r3, sigma = Proof.proof proof in
-       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
-       if List.for_all (fun x -> simple_goal sigma x rest) focused
-       then `Simple focused
-       else `Not
+    let proof = Proof_global.proof_of_state proof in
+    let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
+    let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+    if List.for_all (fun x -> simple_goal sigma x rest) focused
+    then `Simple focused
+    else `Not
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
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 =