[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/printing/proof_diffs.ml b/printing/proof_diffs.ml
index a381266976..b280ce909b 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -553,7 +553,7 @@ open Goal.Set
 let db_goal_map op np ng_to_og =
   let pr_goals title prf =
     Printf.printf "%s: " title;
-    let (goals,_,_,_,sigma) = Proof.proof prf in
+    let Proof.{goals;sigma} = Proof.data prf in
     List.iter (fun g -> Printf.printf "%d -> %s  " (Evar.repr g) (goal_to_evar g sigma)) goals;
     let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in
     List.iter (fun g -> Printf.printf "%d  " (Evar.repr g)) (elements gs);
@@ -626,11 +626,11 @@ let make_goal_map_i op np =
       let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
 
       let oevar_to_og = ref StringMap.empty in
-      let (_,_,_,_,osigma) = Proof.proof op in
+      let Proof.{sigma=osigma} = Proof.data op in
       List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
           (Goal.Set.elements rem_gs);
 
-      let (_,_,_,_,nsigma) = Proof.proof np in
+      let Proof.{sigma=nsigma} = Proof.data np in
       let get_og ng =
         let nevar = goal_to_evar ng nsigma in
         let oevar = StringMap.find nevar nevar_to_oevar in