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, 2 insertions, 2 deletions

diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 751bddc7c4..ad21f663e4 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -220,11 +220,11 @@ let process_goal_diffs diff_goal_map oldp nsigma ng =
   let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
   { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
 
-let export_pre_goals Proof.{ sigma; goals; stack; shelf } process =
+let export_pre_goals Proof.{ sigma; goals; stack } process =
   let process = List.map (process sigma) in
   { Interface.fg_goals       = process goals
   ; Interface.bg_goals       = List.(map (fun (lg,rg) -> process lg, process rg)) stack
-  ; Interface.shelved_goals  = process shelf
+  ; Interface.shelved_goals  = process @@ Evd.shelf sigma
   ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma)
   }