| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-14 | Fix refine and eapply to mark shelved goals as non-resolvable, always | Matthieu Sozeau | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |