diff options
| author | Pierre-Marie Pédrot | 2020-09-01 20:51:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-01 20:51:08 +0200 |
| commit | 8666b46353c1f2c751bb5b6d4e1012783d107ae4 (patch) | |
| tree | be0d256f863dc7ecf1cd2dbbb510c7622282ad24 /printing/printer.ml | |
| parent | 0d30f79268fea18ef99c040a859956f61c3d978a (diff) | |
| parent | 636fe1deaf220f1c30821846343b3a70ef7a078c (diff) | |
Merge PR #12872: Unify the shelves
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 0f635623e7..a1a2d9ae51 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -780,7 +780,8 @@ 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 Proof.{goals; stack; shelf; sigma} = Proof.data p in + let Proof.{goals; stack; sigma} = Proof.data p in + let shelf = Evd.shelf sigma in let given_up = Evd.given_up sigma in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in |