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 --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') 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 -- cgit v1.2.3