From 636fe1deaf220f1c30821846343b3a70ef7a078c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 31 Aug 2020 10:36:32 +0200 Subject: Unify the shelves Before this patch, the proof engine had three notions of shelves: - A local shelf in `proofview` - A global shelf in `Proof.t` - A future shelf in `evar_map` This has lead to a lot of confusion and limitations or bugs, because some components have only a partial view of the shelf: the pretyper can see only the future shelf, tactics can see only the local and future shelves. In particular, this refactoring is needed for #7825. The solution we choose is to move shelf information to the evar map, as a shelf stack (for nested `unshelve` tacticals). Closes #8770. Closes #6292. Co-authored-by: Gaëtan Gilbert --- printing/printer.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'printing/printer.ml') 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 -- cgit v1.2.3