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 --- ide/coqide/idetop.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') 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) } -- cgit v1.2.3