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 <gaetan.gilbert@skyskimmer.net>
---
 vernac/classes.ml       | 2 +-
 vernac/declare.ml       | 4 ++--
 vernac/vernacentries.ml | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 82a1e32a14..02cb60f1cf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -359,7 +359,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
      consequence, we use the low-level primitives to code
      the refinement manually.*)
   let future_goals, sigma = Evd.pop_future_goals sigma in
-  let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in
+  let gls = List.rev future_goals.Evd.FutureGoals.comb in
   let sigma = Evd.push_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
   let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 12d6cb9f49..099a63cf8f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1553,11 +1553,11 @@ let set_used_variables ps l =
   ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
-  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+  let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
   List.length goals +
   List.fold_left (+) 0
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
-  List.length shelf
+  List.length (Evd.shelf sigma)
 
 type proof_object =
   { name : Names.Id.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 540e85621a..6a4c2a626d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -112,7 +112,8 @@ let show_proof ~pstate =
 
 let show_top_evars ~proof =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
-  let Proof.{goals;shelf;sigma} = Proof.data proof in
+  let Proof.{goals; sigma} = Proof.data proof in
+  let shelf = Evd.shelf sigma in
   let given_up = Evar.Set.elements @@ Evd.given_up sigma in
   pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
 
-- 
cgit v1.2.3