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 <gaetan.gilbert@skyskimmer.net>

1 files changed, 0 insertions, 2 deletions

diff --git a/proofs/proof.mli b/proofs/proof.mli
index ffb8380147..f487595dac 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -43,8 +43,6 @@ type data =
   (** Entry for the proofview *)
   ; stack : (Evar.t list * Evar.t list) list
   (** A representation of the focus stack *)
-  ; shelf : Evar.t list
-  (** A representation of the shelf  *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool;