diff options
| author | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
| commit | 6f12c3e3ccce7028abb492f804d30ba0bef58f06 (patch) | |
| tree | db89fb070eead9bcf14880a9b3d3672b0f5bbf85 /proofs | |
| parent | 215d3013312309d47dae01b66b1781b572d30783 (diff) | |
| parent | fbe0ea439ed3cf2ad933bd6094a36b5cebc5bd19 (diff) | |
Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index dcff5e2b6c..ac410a958f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -75,6 +75,8 @@ let generic_refine ~typecheck f gl = let future_goals, sigma = Evd.pop_future_goals sigma in (* Select the goals *) let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in + let shelf = Evd.shelf sigma in + let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> |