| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix bug #5043: [Admitted] lemmas pick up section variables. |  Pierre-Marie Pédrot | 2016-08-31 |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |