aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/printer.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 075b03b7d..ba31b72d6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -828,7 +828,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
let pr_nth_open_subgoal n =
let pf = Proof_global.give_me_the_proof () in
- let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
pr_subgoal n sigma gls
let pr_goal_by_id id =