| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-28 | [stm] Use Default Proof Using only with Proof | Tej Chajed | |
| Fixes #11608. This means -vos doesn't skip proofs for definitions that end with Qed but don't include Proof and rely on a Set Default Proof Using. However, this fixes the bug where this pattern would instead hang, due to #11564. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |