| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-13 | Return of Refine Instance as an attribute. | Gaëtan Gilbert | |
| We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |