| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-14 | Fixes #12234 (wrong environment for Show Proof). | Hugo Herbelin | |
| We take the env of the current goal with the context replaced with section variables. In practice, this is the global env, but, maybe, one day, a goal state will have its own env. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |