| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Test for #4035 (dependent destruction from Ltac). |  Hugo Herbelin | 2015-03-07 |
| | | |||
| * | Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." |  Maxime Dénès | 2015-02-26 |
| | | | | | | | | | | This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035. | ||
| * | Fixing bug #4035 (support for dependent destruction within ltac code). | Hugo Herbelin | 2015-02-16 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |