diff options
| author | Maxime Dénès | 2020-06-11 18:51:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (patch) | |
| tree | b6937b47990e5f76b3f9a5b0fc8999754334ce26 /proofs/refine.ml | |
| parent | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (diff) | |
Move given_up goals to evar_map
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 8909b9639d..4244a9c900 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -75,7 +75,7 @@ let generic_refine ~typecheck f gl = let sigma = Evd.restore_future_goals sigma prev_future_goals in (* Select the goals *) let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in - let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in + let comb,shelf,evkmain = Evd.dispatch_future_goals evs in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> @@ -102,7 +102,6 @@ let generic_refine ~typecheck f gl = Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> Proofview.Unsafe.tclPUTSHELF shelf <*> - Proofview.Unsafe.tclPUTGIVENUP given_up <*> Proofview.tclUNIT v end |