diff options
| author | Maxime Dénès | 2020-08-31 10:36:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-01 16:20:36 +0200 |
| commit | 636fe1deaf220f1c30821846343b3a70ef7a078c (patch) | |
| tree | be0d256f863dc7ecf1cd2dbbb510c7622282ad24 /proofs/refine.ml | |
| parent | 0d30f79268fea18ef99c040a859956f61c3d978a (diff) | |
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>
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 51d6c923b6..dcff5e2b6c 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -92,7 +92,6 @@ let generic_refine ~typecheck f gl = in (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in - let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in @@ -100,7 +99,6 @@ let generic_refine ~typecheck f gl = Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> - Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*> Proofview.tclUNIT v end |