diff options
| author | Matthieu Sozeau | 2019-09-12 11:41:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-12-14 12:21:20 +0100 |
| commit | 40323e4258d5232226d0be277f53bb5462bac417 (patch) | |
| tree | e0d8baa2ba8a0f4bd4695c1c0703b3c243b906c0 /proofs/refine.mli | |
| parent | dd47dfc29f4b38dd2b1745ecbf452c3cd459b89b (diff) | |
Fix refine and eapply to mark shelved goals as non-resolvable, always
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
Diffstat (limited to 'proofs/refine.mli')
| -rw-r--r-- | proofs/refine.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index bdcccae805..269382489d 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -25,7 +25,8 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. + Shelved evars and goals are all marked as unresolvable for typeclasses. *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic |