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 --- engine/termops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 7579631313..ac6870a39e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -301,10 +301,12 @@ let pr_evar_map_gen with_univs pr_evars env sigma = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma + and shelf = + str "SHELF:" ++ brk (0, 1) ++ Evd.pr_shelf sigma ++ fnl () and future_goals = str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl () in - evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ shelf ++ future_goals let pr_evar_list env sigma l = let open Evd in -- cgit v1.2.3