| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-08 | Standardize handling of Automatic Introduction. | Jasper Hugunin | |
| This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |