Merge PR #9172: [proof] Rework proof interface.

3 files changed, 11 insertions, 11 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
diff --git a/printing/printer.mli b/printing/printer.mli
index 357f30d1f4..fd4682a086 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -182,7 +182,7 @@ val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
-val pr_evars_int           : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars_int           : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
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