| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-07 | Tactic subst now inactive on section variables occurring indirectly in goal. | Hugo Herbelin | |
| This is saner behavior making subst reversible, as discussed in #12139. This also fixes #10812 and #12139. In passing, we also simplify a bit the code of "subst_all". | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |