| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Passing around the flag for injection so that tactics calling inj at |  Hugo Herbelin | 2017-10-26 |
| ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |