[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, 7 insertions, 7 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index b80133b171..be0139da06 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -546,10 +546,10 @@ let rec pr_evars_int_hd pr sigma i = function
       (hov 0 (pr i evk evi)) ++
       (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest)
 
-let pr_evars_int sigma ~shelf ~givenup i evs =
+let pr_evars_int sigma ~shelf ~given_up i evs =
   let pr_status i =
     if List.mem i shelf then str " (shelved)"
-    else if List.mem i givenup then str " (given up)"
+    else if List.mem i given_up then str " (given up)"
     else mt () in
   pr_evars_int_hd
     (fun i evk evi ->
@@ -761,7 +761,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
 	if Evar.Map.is_empty exl then
 	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
 	else
-          let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in
+          let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
 	  v 0 ((str "No more subgoals,"
                 ++ str " but there are non-instantiated existential variables:"
 	        ++ cut () ++ (hov 0 pei)
@@ -789,7 +789,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
      straightforward, but seriously, [Proof.proof] should return
      [evar_info]-s instead. *)
   let p = proof in
-  let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in
+  let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in
   let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
@@ -821,7 +821,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
      let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
      let os_map = match oproof with
        | Some op when diffs ->
-         let (_,_,_,_, osigma) = Proof.proof op in
+         let Proof.{sigma=osigma} = Proof.data op in
          let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
          Some (osigma, diff_goal_map)
        | _ -> None
@@ -834,8 +834,8 @@ let pr_open_subgoals ~proof =
   pr_open_subgoals_diff proof
 
 let pr_nth_open_subgoal ~proof n =
-  let gls,_,_,_,sigma = Proof.proof proof in
-  pr_subgoal n sigma gls
+  let Proof.{goals;sigma} = Proof.data proof in
+  pr_subgoal n sigma goals
 
 let pr_goal_by_id ~proof id =
   try