| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. |  Pierre-Marie Pédrot | 2016-09-30 |
| This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |